Merge remote-tracking branch 'upstream/master' into release-lib-cleanup

75 files changed, 1687 insertions, 2319 deletions

diff --git a/pkgs/applications/science/astronomy/gildas/default.nix b/pkgs/applications/science/astronomy/gildas/default.nix
index ee19077065e0..802f558731a8 100644
--- a/pkgs/applications/science/astronomy/gildas/default.nix
+++ b/pkgs/applications/science/astronomy/gildas/default.nix
@@ -7,13 +7,16 @@ let
 in
 
 stdenv.mkDerivation rec {
-  srcVersion = "aug18a";
-  version = "20180801_a";
+  srcVersion = "oct18b";
+  version = "20181001_b";
   name = "gildas-${version}";
 
   src = fetchurl {
-    url = "http://www.iram.fr/~gildas/dist/gildas-src-${srcVersion}.tar.gz";
-    sha256 = "0mg3wijrj8x1p912vkgrhxbypjx7aj9b1492yxvq2y3fxban6bj1";
+    # For each new release, the upstream developers of Gildas move the
+    # source code of the previous release to a different directory
+    urls = [ "http://www.iram.fr/~gildas/dist/gildas-src-${srcVersion}.tar.gz"
+      "http://www.iram.fr/~gildas/dist/archive/gildas/gildas-src-${srcVersion}.tar.gz" ];
+    sha256 = "1q54q7y4zdax9vr28pvmy5g34kyr92jr3v1rkpjw7lxjafyqwy27";
   };
 
   enableParallelBuilding = true;
@@ -22,7 +25,9 @@ stdenv.mkDerivation rec {
 
   buildInputs = [ gtk2-x11 lesstif cfitsio python27Env ];
 
-  patches = [ ./wrapper.patch ./return-error-code.patch ./clang.patch ./aarch64.patch ];
+  patches = [ ./wrapper.patch ./clang.patch ./aarch64.patch ];
+
+  NIX_CFLAGS_COMPILE = stdenv.lib.optionalString stdenv.cc.isClang "-Wno-unused-command-line-argument";
 
   configurePhase=''
     substituteInPlace admin/wrapper.sh --replace '%%OUT%%' $out
diff --git a/pkgs/applications/science/astronomy/gildas/return-error-code.patch b/pkgs/applications/science/astronomy/gildas/return-error-code.patch
deleted file mode 100644
index f0bd7da9354e..000000000000
--- a/pkgs/applications/science/astronomy/gildas/return-error-code.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-diff --new-file -r -u gildas-src-dec17a.orig/admin/gildas-env.sh gildas-src-dec17a/admin/gildas-env.sh
---- gildas-src-dec17a.orig/admin/gildas-env.sh	2017-10-24 11:39:18.000000000 +0200
-+++ gildas-src-dec17a/admin/gildas-env.sh	2017-12-01 11:17:32.051953670 +0100
-@@ -1010,6 +1010,9 @@
-     gagenv_message "$gagenv_errors error(s) and $gagenv_warnings warning(s) detected"
-     if [ $gagenv_errors -ne 0 ]; then
-         gagenv_message "GILDAS will not compile"
-+	gagenv_clean
-+        echo
-+        \return 1
-     elif [ $gagenv_warnings -ne 0 ]; then
-         gagenv_message "GILDAS will compile with some optional features disabled"
-     else
diff --git a/pkgs/applications/science/biology/bowtie2/default.nix b/pkgs/applications/science/biology/bowtie2/default.nix
index 675c7d4eb0b4..73f70efc14d1 100644
--- a/pkgs/applications/science/biology/bowtie2/default.nix
+++ b/pkgs/applications/science/biology/bowtie2/default.nix
@@ -2,14 +2,14 @@
 
 stdenv.mkDerivation rec {
   pname = "bowtie2";
-  version = "2.3.4.2";
+  version = "2.3.4.3";
   name = "${pname}-${version}";
 
   src = fetchFromGitHub {
     owner = "BenLangmead";
     repo = pname;
     rev = "v${version}";
-    sha256 = "1gsfaf7rjg4nwhs7vc1vf63xd5r5v1yq58w7x3barycplzbvixzz";
+    sha256 = "1zl3cf327y2p7p03cavymbh7b00djc7lncfaqih33n96iy9q8ibp";
   };
 
   buildInputs = [ zlib tbb ];
diff --git a/pkgs/applications/science/biology/hisat2/default.nix b/pkgs/applications/science/biology/hisat2/default.nix
new file mode 100644
index 000000000000..9ccf54a81133
--- /dev/null
+++ b/pkgs/applications/science/biology/hisat2/default.nix
@@ -0,0 +1,49 @@
+{stdenv, fetchurl, unzip, which, python}:
+
+stdenv.mkDerivation rec {
+  name = "hisat2-${version}";
+  version = "2.1.0";
+
+  src = fetchurl {
+    url = "ftp://ftp.ccb.jhu.edu/pub/infphilo/hisat2/downloads/hisat2-${version}-source.zip";
+    sha256 = "10g73sdf6vqqfhhd92hliw7bbpkb8v4pp5012r5l21zws7p7d8l9";
+  };
+
+  buildInputs = [ unzip  which python ];
+
+  installPhase = ''
+    mkdir -p $out/bin
+    cp hisat2 \
+       hisat2-inspect-l \
+       hisat2-build-s \
+       hisat2-align-l \
+       hisat2-inspect \
+       hisat2-align-s \
+       hisat2-inspect-s \
+       hisat2-build-l \
+       hisat2-build \
+       extract_exons.py \
+       extract_splice_sites.py \
+       hisat2_extract_exons.py \
+       hisat2_extract_snps_haplotypes_UCSC.py \
+       hisat2_extract_snps_haplotypes_VCF.py \
+       hisat2_extract_splice_sites.py \
+       hisat2_simulate_reads.py \
+       hisatgenotype_build_genome.py \
+       hisatgenotype_extract_reads.py \
+       hisatgenotype_extract_vars.py \
+       hisatgenotype_hla_cyp.py \
+       hisatgenotype_locus.py \
+       hisatgenotype.py \
+       $out/bin
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Graph based aligner";
+    license = licenses.gpl3;
+    homepage = https://ccb.jhu.edu/software/hisat2/index.shtml;
+    maintainers = with maintainers; [ jbedo ];
+    platforms = [ "x86_64-linux" "i686-linux" ];
+  };
+
+}
diff --git a/pkgs/applications/science/biology/picard-tools/default.nix b/pkgs/applications/science/biology/picard-tools/default.nix
index 0ddbdab4c1b1..e825d1e8454f 100644
--- a/pkgs/applications/science/biology/picard-tools/default.nix
+++ b/pkgs/applications/science/biology/picard-tools/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   name = "picard-tools-${version}";
-  version = "2.18.11";
+  version = "2.18.14";
 
   src = fetchurl {
     url = "https://github.com/broadinstitute/picard/releases/download/${version}/picard.jar";
-    sha256 = "03wkyz3bjx3n8bwambhz9lr09271r1wxycmx4p7m2naqs4afxb89";
+    sha256 = "0xc5mqifav2j4zbln04q07wjlzpwp3w0y5iv5bkp4v5486cp2ha9";
   };
 
   buildInputs = [ jre makeWrapper ];
diff --git a/pkgs/applications/science/biology/platypus/default.nix b/pkgs/applications/science/biology/platypus/default.nix
index 2947515652e2..323ca90f0a2a 100644
--- a/pkgs/applications/science/biology/platypus/default.nix
+++ b/pkgs/applications/science/biology/platypus/default.nix
@@ -4,13 +4,13 @@ let python = python27.withPackages (ps: with ps; [ cython ]);
 
 in stdenv.mkDerivation rec {
   name = "platypus-unstable-${version}";
-  version = "2017-03-07";
+  version = "2018-07-22";
 
   src = fetchFromGitHub {
     owner = "andyrimmer";
     repo = "Platypus";
-    rev = "cbbd914";
-    sha256 = "0xgj3pl7n4c12j5pp5qyjfk4rsvb5inwzrpcbhdf3br5f3mmdsb9";
+    rev = "3e72641c69800da0cd4906b090298e654d316ee1";
+    sha256 = "0nah6r54b8xm778gqyb8b7rsd76z8ji4g73sm6rvpw5s96iib1vw";
   };
 
   buildInputs = [ htslib python zlib makeWrapper ];
diff --git a/pkgs/applications/science/biology/samtools/default.nix b/pkgs/applications/science/biology/samtools/default.nix
index 87e708526ef7..c4b4bb522c40 100644
--- a/pkgs/applications/science/biology/samtools/default.nix
+++ b/pkgs/applications/science/biology/samtools/default.nix
@@ -3,11 +3,11 @@
 stdenv.mkDerivation rec {
   name = "${pname}-${version}";
   pname = "samtools";
-  version = "1.8";
+  version = "1.9";
 
   src = fetchurl {
     url = "https://github.com/samtools/samtools/releases/download/${version}/${name}.tar.bz2";
-    sha256 = "05myg7bs90i68qbqab9cdg9rqj2xh39azibrx82ipzc5kcfvqhn9";
+    sha256 = "10ilqbmm7ri8z431sn90lvbjwizd0hhkf9rcqw8j823hf26nhgq8";
   };
 
   nativeBuildInputs = [ perl ];
diff --git a/pkgs/applications/science/biology/seaview/default.nix b/pkgs/applications/science/biology/seaview/default.nix
new file mode 100644
index 000000000000..17cf903ae49c
--- /dev/null
+++ b/pkgs/applications/science/biology/seaview/default.nix
@@ -0,0 +1,41 @@
+{ stdenv, fetchurl, coreutils, fltk, libjpeg }:
+
+stdenv.mkDerivation rec {
+  version = "4.7";
+  name = "seaview-${version}";
+
+  src = fetchurl {
+    url = "ftp://pbil.univ-lyon1.fr/pub/mol_phylogeny/seaview/archive/seaview_${version}.tar.gz";
+    sha256 = "0fhyq7dcn0izhwcfin9ajsr7kmmsqm9f1np1rmhzg4digfwqb29n";
+  };
+
+  buildInputs = [ fltk libjpeg ];
+
+  patchPhase = "sed -i 's#PATH=/bin:/usr/bin rm#'${coreutils}/bin/rm'#' seaview.cxx";
+  installPhase = "mkdir -p $out/bin; cp seaview $out/bin";
+
+  meta = with stdenv.lib; {
+    description = "GUI for molecular phylogeny";
+    longDescription = ''
+      SeaView is a multiplatform, graphical user interface for multiple sequence alignment and molecular phylogeny.
+        - SeaView reads and writes various file formats (NEXUS, MSF, CLUSTAL, FASTA, PHYLIP, MASE, Newick) of DNA and protein sequences and of phylogenetic trees.
+        - SeaView drives programs muscle or Clustal Omega for multiple sequence alignment, and also allows to use any external alignment algorithm able to read and write FASTA-formatted files.
+        - Seaview drives the Gblocks program to select blocks of evolutionarily conserved sites.
+        - SeaView computes phylogenetic trees by
+          + parsimony, using PHYLIP's dnapars/protpars algorithm,
+          + distance, with NJ or BioNJ algorithms on a variety of evolutionary distances,
+          + maximum likelihood, driving program PhyML 3.1.
+        - Seaview can use the Transfer Bootstrap Expectation method to compute the bootstrap support of PhyML and distance trees.
+        - SeaView prints and draws phylogenetic trees on screen, SVG, PDF or PostScript files.
+        - SeaView allows to download sequences from EMBL/GenBank/UniProt using the Internet.
+
+      Seaview is published in:
+
+          Gouy M., Guindon S. & Gascuel O. (2010) SeaView version 4 : a multiplatform graphical user interface for sequence alignment and phylogenetic tree building. Molecular Biology and Evolution 27(2):221-224.
+    '';
+    homepage = http://doua.prabi.fr/software/seaview;
+    license = licenses.gpl3;
+    maintainers = [ maintainers.iimog ];
+    platforms = platforms.linux;
+  };
+}
diff --git a/pkgs/applications/science/biology/star/default.nix b/pkgs/applications/science/biology/star/default.nix
index f52df902db6a..e22043d9eb9c 100644
--- a/pkgs/applications/science/biology/star/default.nix
+++ b/pkgs/applications/science/biology/star/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   name = "star-${version}";
-  version = "2.6.0c";
+  version = "2.6.1c";
 
   src = fetchFromGitHub {
     repo = "STAR";
     owner = "alexdobin";
     rev = version;
-    sha256 = "04cj6jw8d9q6lk9c78wa4fky6jdlicf1d13plq7182h8vqiz8p59";
+    sha256 = "0macdbxa0v5xplag83fpdhfpyhnqncmi9wf9r92wa7w8zkln12vd";
   };
 
   sourceRoot = "source/source";
diff --git a/pkgs/applications/science/chemistry/jmol/default.nix b/pkgs/applications/science/chemistry/jmol/default.nix
index d5dae364cc3d..dab30e90f4d8 100644
--- a/pkgs/applications/science/chemistry/jmol/default.nix
+++ b/pkgs/applications/science/chemistry/jmol/default.nix
@@ -17,7 +17,7 @@ let
   };
 in
 stdenv.mkDerivation rec {
-  version = "14.29.17";
+  version = "14.29.26";
   pname = "jmol";
   name = "${pname}-${version}";
 
@@ -25,7 +25,7 @@ stdenv.mkDerivation rec {
     baseVersion = "${lib.versions.major version}.${lib.versions.minor version}";
   in fetchurl {
     url = "mirror://sourceforge/jmol/Jmol/Version%20${baseVersion}/Jmol%20${version}/Jmol-${version}-binary.tar.gz";
-    sha256 = "1dnxbvi8ha9z2ldymkjpxydd216afv6k7fdp3j70sql10zgy0isk";
+    sha256 = "0a728lwqbbnm5v2spi5rbqy3xldbcf2gcsf48rkq3p43laps3630";
   };
 
   patchPhase = ''
diff --git a/pkgs/applications/science/chemistry/openmolcas/default.nix b/pkgs/applications/science/chemistry/openmolcas/default.nix
index 5e1628a4fba7..70e79023c0ff 100644
--- a/pkgs/applications/science/chemistry/openmolcas/default.nix
+++ b/pkgs/applications/science/chemistry/openmolcas/default.nix
@@ -5,8 +5,8 @@
 } :
 
 let
-  version = "20180529";
-  gitLabRev = "b6b9ceffccae0dd7f14c099468334fee0b1071fc";
+  version = "18.09";
+  gitLabRev = "v${version}";
 
   python = python3.withPackages (ps : with ps; [ six pyparsing ]);
 
@@ -17,7 +17,7 @@ in stdenv.mkDerivation {
     owner = "Molcas";
     repo = "OpenMolcas";
     rev = gitLabRev;
-    sha256 = "1wbjjdv07lg1x4kdnf28anyrjgy33gdgrd5d7zi1c97nz7vhdjaz";
+    sha256 = "1di1ygifx7ycfpwh25mv76xlv15wqfdmqzjsg5nani2d5z0arri2";
   };
 
   nativeBuildInputs = [ perl cmake texlive.combined.scheme-minimal makeWrapper ];
diff --git a/pkgs/applications/science/chemistry/quantum-espresso/default.nix b/pkgs/applications/science/chemistry/quantum-espresso/default.nix
new file mode 100644
index 000000000000..7a7f1b3596d3
--- /dev/null
+++ b/pkgs/applications/science/chemistry/quantum-espresso/default.nix
@@ -0,0 +1,49 @@
+{ stdenv, fetchurl
+, gfortran, fftw, openblas
+, mpi ? null
+}:
+
+stdenv.mkDerivation rec {
+  version = "6.3";
+  name = "quantum-espresso-${version}";
+
+  src = fetchurl {
+    url = "https://gitlab.com/QEF/q-e/-/archive/qe-${version}/q-e-qe-${version}.tar.gz";
+    sha256 = "1738z3nhkzcrgnhnfg1r4lipbwvcrcprwhzjbjysnylmzbzwhrs0";
+  };
+
+  passthru = {
+    inherit mpi;
+  };
+
+  preConfigure = ''
+    patchShebangs configure
+  '';
+
+  # remove after 6.3 version:
+  # makefile needs to ignore install directory easier than applying patch
+  preInstall = ''
+    printf "\n.PHONY: install\n" >> Makefile
+  '';
+
+  buildInputs = [ fftw openblas gfortran ]
+    ++ (stdenv.lib.optionals (mpi != null) [ mpi ]);
+
+configureFlags = if (mpi != null) then [ "LD=${mpi}/bin/mpif90" ] else [ "LD=${gfortran}/bin/gfortran" ];
+
+  makeFlags = [ "all" ];
+
+  meta = with stdenv.lib; {
+    description = "Electronic-structure calculations and materials modeling at the nanoscale";
+    longDescription = ''
+        Quantum ESPRESSO is an integrated suite of Open-Source computer codes for
+        electronic-structure calculations and materials modeling at the
+        nanoscale. It is based on density-functional theory, plane waves, and
+        pseudopotentials.
+      '';
+    homepage = https://www.quantum-espresso.org/;
+    license = licenses.gpl2;
+    platforms = [ "x86_64-linux" ];
+    maintainers = [ maintainers.costrouc ];
+  };
+}
diff --git a/pkgs/applications/science/chemistry/siesta/default.nix b/pkgs/applications/science/chemistry/siesta/default.nix
new file mode 100644
index 000000000000..eb17a68b8aae
--- /dev/null
+++ b/pkgs/applications/science/chemistry/siesta/default.nix
@@ -0,0 +1,69 @@
+{ stdenv, fetchurl
+, gfortran, openblas
+, mpi ? null, scalapack
+}:
+
+stdenv.mkDerivation rec {
+  version = "4.1-b3";
+  name = "siesta-${version}";
+
+  src = fetchurl {
+    url = "https://launchpad.net/siesta/4.1/4.1-b3/+download/siesta-4.1-b3.tar.gz";
+    sha256 = "1450jsxj5aifa0b5fcg7mxxq242fvqnp4zxpgzgbkdp99vrp06gm";
+  };
+
+  passthru = {
+    inherit mpi;
+  };
+
+  buildInputs = [ openblas gfortran ]
+    ++ (stdenv.lib.optionals (mpi != null) [ mpi scalapack ]);
+
+  enableParallelBuilding = true;
+
+  # Must do manualy becuase siesta does not do the regular
+  # ./configure; make; make install
+  configurePhase = ''
+    cd Obj
+    sh ../Src/obj_setup.sh
+    cp gfortran.make arch.make
+  '';
+
+  preBuild = if (mpi != null) then ''
+    makeFlagsArray=(
+        CC="mpicc" FC="mpifort"
+        FPPFLAGS="-DMPI" MPI_INTERFACE="libmpi_f90.a" MPI_INCLUDE="."
+        COMP_LIBS="" LIBS="-lopenblas -lscalapack"
+    );
+  '' else ''
+    makeFlagsArray=(
+      COMP_LIBS="" LIBS="-lopenblas"
+    );
+  '';
+
+  installPhase = ''
+    mkdir -p $out/bin
+    cp -a siesta $out/bin
+  '';
+
+  meta = with stdenv.lib; {
+    description = "A first-principles materials simulation code using DFT";
+    longDescription = ''
+         SIESTA is both a method and its computer program
+         implementation, to perform efficient electronic structure
+         calculations and ab initio molecular dynamics simulations of
+         molecules and solids. SIESTA's efficiency stems from the use
+         of strictly localized basis sets and from the implementation
+         of linear-scaling algorithms which can be applied to suitable
+         systems. A very important feature of the code is that its
+         accuracy and cost can be tuned in a wide range, from quick
+         exploratory calculations to highly accurate simulations
+         matching the quality of other approaches, such as plane-wave
+         and all-electron methods.
+      '';
+    homepage = https://www.quantum-espresso.org/;
+    license = licenses.gpl2;
+    platforms = [ "x86_64-linux" ];
+    maintainers = [ maintainers.costrouc ];
+  };
+}
diff --git a/pkgs/applications/science/electronics/gtkwave/default.nix b/pkgs/applications/science/electronics/gtkwave/default.nix
index c0048740193f..3f664006cd0f 100644
--- a/pkgs/applications/science/electronics/gtkwave/default.nix
+++ b/pkgs/applications/science/electronics/gtkwave/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   name = "gtkwave-${version}";
-  version = "3.3.93";
+  version = "3.3.95";
 
   src = fetchurl {
     url    = "mirror://sourceforge/gtkwave/${name}.tar.gz";
-    sha256 = "0a92zlwvshp75k7cv11rc4ab11fzsy0a5qfvxkh0bjvrq1k946ys";
+    sha256 = "1999wnipah1ncvjzjf95pfdrvgq1kd6hli8xlaj2hfjka8pamfaf";
   };
 
   nativeBuildInputs = [ pkgconfig ];
diff --git a/pkgs/applications/science/electronics/kicad/default.nix b/pkgs/applications/science/electronics/kicad/default.nix
index 3e783d2e177c..c92da3eeb292 100644
--- a/pkgs/applications/science/electronics/kicad/default.nix
+++ b/pkgs/applications/science/electronics/kicad/default.nix
@@ -36,8 +36,7 @@ stdenv.mkDerivation rec {
     ++ optional (ngspiceSupport) "-DKICAD_SPICE=ON";
 
   nativeBuildInputs = [
-    # https://www.mail-archive.com/kicad-developers@lists.launchpad.net/msg29840.html
-    (cmake.override {majorVersion = "3.10";})
+    cmake
     doxygen
     pkgconfig
     wrapGAppsHook
diff --git a/pkgs/applications/science/electronics/kicad/unstable.nix b/pkgs/applications/science/electronics/kicad/unstable.nix
index e43fd59e0431..a9a4c32a0b45 100644
--- a/pkgs/applications/science/electronics/kicad/unstable.nix
+++ b/pkgs/applications/science/electronics/kicad/unstable.nix
@@ -38,8 +38,7 @@ stdenv.mkDerivation rec {
       "-DCMAKE_CXX_FLAGS=-I${wxPython}/include/wx-3.0"
     ];
 
-  # https://www.mail-archive.com/kicad-developers@lists.launchpad.net/msg29840.html
-  nativeBuildInputs = [ (cmake.override {majorVersion = "3.10";}) doxygen  pkgconfig ];
+  nativeBuildInputs = [ cmake doxygen pkgconfig ];
   buildInputs = [
     libGLU_combined zlib libX11 wxGTK pcre libXdmcp gettext glew glm libpthreadstubs
     cairo curl openssl boost
diff --git a/pkgs/applications/science/electronics/verilator/default.nix b/pkgs/applications/science/electronics/verilator/default.nix
index fd6240fe1b21..dd31f28db313 100644
--- a/pkgs/applications/science/electronics/verilator/default.nix
+++ b/pkgs/applications/science/electronics/verilator/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   name    = "verilator-${version}";
-  version = "3.926";
+  version = "4.004";
 
   src = fetchurl {
     url    = "https://www.veripool.org/ftp/${name}.tgz";
-    sha256 = "0f4ajj1gmxskid61qj1ql1rzc3cmn1x2fpgqrbg7x3gszz61c9gr";
+    sha256 = "1nkdmz4bm1v2xarajf2g3z5vb2611a4fkvpgjxac4xrja5r8wpwk";
   };
 
   enableParallelBuilding = true;
diff --git a/pkgs/applications/science/geometry/drgeo/default.nix b/pkgs/applications/science/geometry/drgeo/default.nix
index 8db1beedebbb..e233b91bbc91 100644
--- a/pkgs/applications/science/geometry/drgeo/default.nix
+++ b/pkgs/applications/science/geometry/drgeo/default.nix
@@ -20,8 +20,10 @@ stdenv.mkDerivation rec {
     cp drgeo.desktop.in drgeo.desktop
   '';
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "Interactive geometry program";
-    platforms = stdenv.lib.platforms.linux;
+    homepage = https://sourceforge.net/projects/ofset;
+    license = licenses.gpl2;
+    platforms = platforms.linux;
   };
 }
diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
index 8cf4bb9b6d25..794430ebbe84 100644
--- a/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -2,21 +2,21 @@
 
 stdenv.mkDerivation rec {
   name = "alt-ergo-${version}";
-  version = "1.30";
+  version = "2.2.0";
 
   src = fetchurl {
     url    = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
     name   = "${name}.tar.gz";
-    sha256 = "025pacb4ax864fn5x8k78mw6hiig4jcazblj18gzxspg4f1l5n1g";
+    sha256 = "106zfgisq6qxr7dlk8z7gi68ly7qff4frn8wab2g8z2nkkwla92w";
   };
 
   buildInputs = with ocamlPackages;
-    [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex ];
+    [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex psmt2-frontend menhir num ];
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
     homepage    = "https://alt-ergo.ocamlpro.com/";
-    license     = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
+    license     = stdenv.lib.licenses.ocamlpro_nc;
     platforms   = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin;
     maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
diff --git a/pkgs/applications/science/logic/cedille/default.nix b/pkgs/applications/science/logic/cedille/default.nix
new file mode 100644
index 000000000000..0817ebe0654b
--- /dev/null
+++ b/pkgs/applications/science/logic/cedille/default.nix
@@ -0,0 +1,50 @@
+{ stdenv, lib, fetchFromGitHub, alex, happy, Agda, agdaIowaStdlib,
+  buildPlatform, buildPackages, ghcWithPackages, fetchpatch }:
+let
+  options-patch =
+    fetchpatch {
+      url = https://github.com/cedille/cedille/commit/ee62b0fabde6c4f7299a3778868519255cc4a64f.patch;
+      name = "options.patch";
+      sha256 = "19xzn9sqpfnfqikqy1x9lb9mb6722kbgvrapl6cf8ckcw8cfj8cz";
+      };
+in
+stdenv.mkDerivation rec {
+  version = "1.0.0";
+  name = "cedille-${version}";
+  src = fetchFromGitHub {
+    owner = "cedille";
+    repo = "cedille";
+    rev = "v${version}";
+    sha256 = "08c2vgg8i6l3ws7hd5gsj89mki36lxm7x7s8hi1qa5gllq04a832";
+  };
+  buildInputs = [ alex happy Agda (ghcWithPackages (ps: [ps.ieee])) ];
+
+  patches = [options-patch];
+
+  LANG = "en_US.UTF-8";
+  LOCALE_ARCHIVE =
+    lib.optionalString (buildPlatform.libc == "glibc")
+      "${buildPackages.glibcLocales}/lib/locale/locale-archive";
+
+  postPatch = ''
+    patchShebangs create-libraries.sh
+    cp -r ${agdaIowaStdlib.src} ial
+    chmod -R 755 ial
+  '';
+
+  outputs = ["out" "lib"];
+
+  installPhase = ''
+    mkdir -p $out/bin
+    mv cedille $out/bin/cedille
+    mv lib $lib
+  '';
+
+  meta = {
+    description = "An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory.";
+    homepage = https://cedille.github.io/;
+    license = stdenv.lib.licenses.mit;
+    maintainers = [ stdenv.lib.maintainers.mpickering ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}
diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix
deleted file mode 100644
index 341267b2cebe..000000000000
--- a/pkgs/applications/science/logic/coq/8.3.nix
+++ /dev/null
@@ -1,82 +0,0 @@
-# - coqide compilation can be disabled by setting lablgtk to null;
-# - The csdp program used for the Micromega tactic is statically referenced.
-#   However, coq can build without csdp by setting it to null.
-#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
-
-{ stdenv, lib, make, fetchurl
-, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null }:
-
-assert lib.versionOlder ocaml.version "4";
-
-let 
-  version = "8.3pl4";
-  buildIde = lablgtk != null;
-  ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  idePatch = if buildIde then ''
-    substituteInPlace scripts/coqmktop.ml --replace \
-    "\"-I\"; \"+lablgtk2\"" \
-    "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
-  '' else "";
-  csdpPatch = if csdp != null then ''
-    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
-    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.search_exe_in_path \"csdp\"" "Some \"${csdp}/bin/csdp\""
-  '' else "";
-in
-
-stdenv.mkDerivation {
-  name = "coq-${version}";
-
-  src = fetchurl {
-    url = "https://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "17d3lmchmqir1rawnr52g78srg4wkd7clzpzfsivxc4y1zp6rwkr";
-  };
-
-  buildInputs = [ make ocaml findlib camlp5 ncurses lablgtk ];
-
-  prefixKey = "-prefix ";
-
-  preConfigure = ''
-    configureFlagsArray=(
-      -opt
-      -camldir ${ocaml}/bin
-      -camlp5dir $(ocamlfind query camlp5)
-      ${ideFlags}
-    )
-  '';
-
-  buildFlags = "world"; # Debug with "world VERBOSE=1";
-
-  patches = [ ./configure.8.3.patch ];
-
-  postPatch = ''
-    UNAME=$(type -tp uname)
-    RM=$(type -tp rm)
-    substituteInPlace configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    ${idePatch}
-    ${csdpPatch}
-  '';
-
-  # This post install step is needed to build ssrcoqide from the ssreflect package
-  # It could be made optional, but I see little harm in including it in the default
-  # distribution -- roconnor
-  # This will likely no longer be necessary for coq >= 8.4. -- roconnor
-  postInstall = if buildIde then ''
-   cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
-  '' else "";
-
-  meta = with stdenv.lib; {
-    description = "Coq proof assistant";
-    longDescription = ''
-      Coq is a formal proof management system.  It provides a formal language
-      to write mathematical definitions, executable algorithms and theorems
-      together with an environment for semi-interactive development of
-      machine-checked proofs.
-    '';
-    homepage = http://coq.inria.fr;
-    license = licenses.lgpl21;
-    branch = "8.3";
-    maintainers = with maintainers; [ roconnor vbgl ];
-    platforms = with platforms; linux;
-  };
-}
diff --git a/pkgs/applications/science/logic/coq/8.4.nix b/pkgs/applications/science/logic/coq/8.4.nix
deleted file mode 100644
index c3da1205ab0c..000000000000
--- a/pkgs/applications/science/logic/coq/8.4.nix
+++ /dev/null
@@ -1,97 +0,0 @@
-# - coqide compilation can be disabled by setting lablgtk to null;
-# - The csdp program used for the Micromega tactic is statically referenced.
-#   However, coq can build without csdp by setting it to null.
-#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
-
-{stdenv, fetchurl, pkgconfig, writeText, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
-
-let
-  version = "8.4pl6";
-  coq-version = "8.4";
-  buildIde = lablgtk != null;
-  ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  csdpPatch = if csdp != null then ''
-    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
-    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
-  '' else "";
-
-self =
-stdenv.mkDerivation {
-  name = "coq-${version}";
-
-  inherit coq-version;
-  inherit ocaml camlp5;
-
-  src = fetchurl {
-    url = "https://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "1mpbj4yf36kpjg2v2sln12i8dzqn8rag6fd07hslj2lpm4qs4h55";
-  };
-
-  nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
-
-  patches = [ ./configure.patch ];
-
-  postPatch = ''
-    UNAME=$(type -tp uname)
-    RM=$(type -tp rm)
-    substituteInPlace configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    ${csdpPatch}
-  '';
-
-  preConfigure = ''
-    configureFlagsArray=(
-      -opt
-      -camldir ${ocaml}/bin
-      -camlp5dir $(ocamlfind query camlp5)
-      ${ideFlags}
-    )
-  '';
-
-  prefixKey = "-prefix ";
-
-  buildFlags = "revision coq coqide";
-
-  setupHook = writeText "setupHook.sh" ''
-    addCoqPath () {
-      if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
-        export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
-      fi
-    }
-
-    addEnvHooks "$targetOffset" addCoqPath
-  '';
-
-  passthru = {
-    inherit findlib;
-    emacsBufferSetup = pkgs: ''
-      ; Propagate coq paths to children
-      (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
-      (inherit-local-permanent coq-dependency-analyzer "${self}/bin/coqdep")
-      (inherit-local-permanent coq-compiler "${self}/bin/coqc")
-      ; If the coq-library path was already set, re-set it based on our current coq
-      (when (fboundp 'get-coq-library-directory)
-        (inherit-local-permanent coq-library-directory (get-coq-library-directory))
-        (coq-prog-args))
-      (mapc (lambda (arg)
-        (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib"))
-          (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)}))
-    '';
-  };
-
-  meta = with stdenv.lib; {
-    description = "Formal proof management system";
-    longDescription = ''
-      Coq is a formal proof management system.  It provides a formal language
-      to write mathematical definitions, executable algorithms and theorems
-      together with an environment for semi-interactive development of
-      machine-checked proofs.
-    '';
-    homepage = http://coq.inria.fr;
-    license = licenses.lgpl21;
-    branch = coq-version;
-    maintainers = with maintainers; [ roconnor thoughtpolice vbgl ];
-    platforms = platforms.unix;
-  };
-}; in self
diff --git a/pkgs/applications/science/logic/coq/configure.8.3.patch b/pkgs/applications/science/logic/coq/configure.8.3.patch
deleted file mode 100644
index 431cccac4b0b..000000000000
--- a/pkgs/applications/science/logic/coq/configure.8.3.patch
+++ /dev/null
@@ -1,1112 +0,0 @@
-diff -Nuar coq-8.3pl3-orig/configure coq-8.3pl3/configure
---- coq-8.3pl3-orig/configure	2011-12-19 22:57:30.000000000 +0100
-+++ coq-8.3pl3/configure	2012-03-17 16:38:16.000000000 +0100
-@@ -395,7 +395,6 @@
- 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
- 	 ocamlmktopexec=$CAMLBIN/ocamlmktop
- 	 ocamlmklibexec=$CAMLBIN/ocamlmklib
--	 camlp4oexec=$CAMLBIN/camlp4o
- esac
- 
- if test ! -f "$CAMLC" ; then
-@@ -628,7 +627,7 @@
-             no)  LABLGTKLIB=+lablgtk2                   # Pour le message
-                  LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
-             yes) LABLGTKLIB="$lablgtkdir"               # Pour le message
--                 LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
-+                 LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
-         esac;;
-     no) LABLGTKINCLUDES="";;
- esac
-diff -Nuar coq-8.3pl3-orig/configure~ coq-8.3pl3/configure~
---- coq-8.3pl3-orig/configure~	1970-01-01 01:00:00.000000000 +0100
-+++ coq-8.3pl3/configure~	2011-12-19 22:57:30.000000000 +0100
-@@ -0,0 +1,1088 @@
-+#!/bin/sh
-+
-+##################################
-+#
-+#  Configuration script for Coq
-+# 
-+##################################
-+
-+VERSION=8.3pl3
-+VOMAGIC=08300
-+STATEMAGIC=58300
-+DATE=`LANG=C date +"%B %Y"`
-+
-+# Create the bin/ directory if non-existent
-+test -d bin || mkdir bin
-+
-+# a local which command for sh
-+which () {
-+IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
-+for i in $PATH; do
-+  if test -z "$i"; then i=.; fi 
-+  if [ -f "$i/$1" ] ; then
-+	IFS=" "
-+        echo "$i/$1"
-+	break
-+  fi
-+done
-+}
-+
-+usage () {
-+    printf "Available options for configure are:\n"
-+    echo "-help"
-+    printf "\tDisplays this help page\n"
-+    echo "-prefix <dir>"
-+    printf "\tSet installation directory to <dir>\n"
-+    echo "-local"
-+    printf "\tSet installation directory to the current source tree\n"
-+    echo "-coqrunbyteflags"
-+    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
-+    echo "-coqtoolsbyteflags"
-+    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
-+    echo "-custom"
-+    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
-+    echo "-src"
-+    printf "\tSpecifies the source directory\n"
-+    echo "-bindir"
-+    echo "-libdir"
-+    echo "-mandir"
-+    echo "-docdir"
-+    printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
-+    echo "-emacslib"
-+    echo "-emacs"
-+    printf "\tSpecifies where emacs files are to be installed\n"
-+    echo "-coqdocdir"
-+    printf "\tSpecifies where Coqdoc style files are to be installed\n"
-+    echo "-camldir"
-+    printf "\tSpecifies the path to the OCaml library\n"
-+    echo "-lablgtkdir"
-+    printf "\tSpecifies the path to the Lablgtk library\n"
-+    echo "-camlp5dir"
-+    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
-+    echo "-arch"
-+    printf "\tSpecifies the architecture\n"
-+    echo "-opt"
-+    printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
-+    echo "-natdynlink (yes|no)"
-+    printf "\tSpecifies whether or not to use dynamic loading of native code\n"
-+    echo "-coqide (opt|byte|no)"
-+    printf "\tSpecifies whether or not to compile Coqide\n"
-+    echo "-browser <command>"
-+    printf "\tUse <command> to open URL %%s\n"
-+    echo "-with-doc (yes|no)"
-+    printf "\tSpecifies whether or not to compile the documentation\n"
-+    echo "-with-geoproof (yes|no)"
-+    printf "\tSpecifies whether or not to use Geoproof binding\n"
-+    echo "-with-cc <file>"
-+    echo "-with-ar <file>"
-+    echo "-with-ranlib <file>"
-+    printf "\tTells configure where to find gcc/ar/ranlib executables\n"
-+    echo "-byte-only"
-+    printf "\tCompiles only bytecode version of Coq\n"
-+    echo "-debug"
-+    printf "\tAdd debugging information in the Coq executables\n"
-+    echo "-profile"
-+    printf "\tAdd profiling information in the Coq executables\n"
-+    echo "-annotate"
-+    printf "\tCompiles Coq with -dtypes option\n"
-+}
-+
-+
-+# Default OCaml binaries
-+bytecamlc=ocamlc
-+nativecamlc=ocamlopt
-+ocamlmklibexec=ocamlmklib
-+ocamlexec=ocaml
-+ocamldepexec=ocamldep
-+ocamldocexec=ocamldoc
-+ocamllexexec=ocamllex
-+ocamlyaccexec=ocamlyacc
-+ocamlmktopexec=ocamlmktop
-+camlp4oexec=camlp4o
-+
-+
-+coq_debug_flag=
-+coq_debug_flag_opt=
-+coq_profile_flag=
-+coq_annotate_flag=
-+best_compiler=opt
-+cflags="-fno-defer-pop -Wall -Wno-unused"
-+natdynlink=yes
-+
-+gcc_exec=gcc
-+ar_exec=ar
-+ranlib_exec=ranlib
-+
-+local=false
-+coqrunbyteflags_spec=no
-+coqtoolsbyteflags_spec=no
-+custom_spec=no
-+src_spec=no
-+prefix_spec=no
-+bindir_spec=no
-+libdir_spec=no
-+mandir_spec=no
-+docdir_spec=no
-+emacslib_spec=no
-+emacs_spec=no
-+camldir_spec=no
-+lablgtkdir_spec=no
-+coqdocdir_spec=no
-+arch_spec=no
-+coqide_spec=no
-+browser_spec=no
-+wwwcoq_spec=no
-+with_geoproof=false
-+with_doc=all
-+with_doc_spec=no
-+force_caml_version=no
-+force_caml_version_spec=no
-+
-+COQSRC=`pwd`
-+
-+# Parse command-line arguments
-+
-+while : ; do
-+  case "$1" in
-+    "") break;;
-+    -help|--help) usage
-+	          exit;;
-+    -prefix|--prefix) prefix_spec=yes
-+                      prefix="$2"
-+		      shift;;
-+    -local|--local) local=true;;
-+    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
-+                                        coqrunbyteflags="$2"
-+                                        shift;;
-+    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
-+                                            coqtoolsbyteflags="$2"
-+                                            shift;;
-+    -custom|--custom) custom_spec=yes
-+                      shift;;
-+    -src|--src) src_spec=yes
-+                COQSRC="$2"
-+	        shift;;
-+    -bindir|--bindir) bindir_spec=yes
-+                      bindir="$2"
-+		      shift;;
-+    -libdir|--libdir) libdir_spec=yes
-+                      libdir="$2"
-+		      shift;;
-+    -mandir|--mandir) mandir_spec=yes
-+                      mandir="$2"
-+		      shift;;
-+    -docdir|--docdir) docdir_spec=yes
-+                      docdir="$2"
-+		      shift;;
-+    -emacslib|--emacslib) emacslib_spec=yes
-+                          emacslib="$2"
-+			  shift;;
-+    -emacs |--emacs) emacs_spec=yes
-+		     emacs="$2"
-+		     shift;;
-+    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
-+	              coqdocdir="$2"
-+		      shift;;
-+    -camldir|--camldir) camldir_spec=yes
-+	                camldir="$2"
-+			shift;;
-+    -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
-+	                lablgtkdir="$2"
-+			shift;;
-+    -camlp5dir|--camlp5dir)
-+	                camlp5dir="$2"
-+			shift;;
-+    -arch|--arch) arch_spec=yes
-+                  arch=$2
-+		  shift;;
-+    -opt|--opt) bytecamlc=ocamlc.opt
-+                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
-+                nativecamlc=ocamlopt.opt;;
-+    -natdynlink|--natdynlink) case "$2" in
-+	                  yes) natdynlink=yes;;
-+                          *) natdynlink=no
-+                        esac
-+                        shift;;
-+    -coqide|--coqide) coqide_spec=yes
-+		      case "$2" in
-+			  byte|opt) COQIDE=$2;;
-+			  *) COQIDE=no
-+		      esac
-+		      shift;;
-+    -browser|--browser) browser_spec=yes
-+		      BROWSER=$2
-+		      shift;;
-+    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
-+                      WWWCOQ=$2
-+                      shift;;
-+    -with-doc|--with-doc) with_doc_spec=yes
-+		      case "$2" in
-+			  yes|all) with_doc=all;;
-+			  *) with_doc=no
-+		      esac
-+		      shift;;
-+    -with-geoproof|--with-geoproof) 
-+	  case "$2" in
-+	      yes) with_geoproof=true;;
-+	      no) with_geoproof=false;;
-+	  esac
-+	  shift;;
-+    -with-cc|-with-gcc|--with-cc|--with-gcc) 
-+	  gcc_spec=yes
-+	  gcc_exec=$2
-+	  shift;;
-+    -with-ar|--with-ar) 
-+	  ar_spec=yes
-+	  ar_exec=$2
-+	  shift;;
-+    -with-ranlib|--with-ranlib) 
-+	  ranlib_spec=yes
-+	  ranlib_exec=$2
-+	  shift;;
-+    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
-+    -debug|--debug) coq_debug_flag=-g;;
-+    -profile|--profile) coq_profile_flag=-p;;
-+    -annotate|--annotate) coq_annotate_flag=-dtypes;;
-+    -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) 
-+          force_caml_version_spec=yes
-+	  force_caml_version=yes;;
-+    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
-+  esac
-+  shift
-+done
-+
-+if [ $prefix_spec = yes -a $local = true ] ; then
-+  echo "Options -prefix and -local are incompatible."
-+  echo "Configure script failed!"
-+  exit 1
-+fi
-+
-+# compile date
-+DATEPGM=`which date`
-+case $DATEPGM in
-+    "") echo "I can't find the program \"date\" in your path."
-+        echo "Please give me the current date"
-+	read COMPILEDATE;;
-+    *)  COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
-+esac
-+
-+# Architecture
-+
-+case $arch_spec in
-+    no) 
-+    # First we test if we are running a Cygwin system
-+    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
-+	ARCH="win32"
-+    else
-+	# If not, we determine the architecture
-+	if test -x /bin/arch ; then
-+ 	    ARCH=`/bin/arch`
-+ 	elif test -x /usr/bin/arch ; then
-+ 	    ARCH=`/usr/bin/arch`
-+ 	elif test -x /usr/ucb/arch ; then
-+ 	    ARCH=`/usr/ucb/arch`
-+ 	elif test -x /bin/uname ; then
-+ 	    ARCH=`/bin/uname -s`
-+ 	elif test -x /usr/bin/uname ; then
-+ 	    ARCH=`/usr/bin/uname -s`
-+	else
-+	    echo "I can not automatically find the name of your architecture."
-+	    printf "%s"\
-+		"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
-+	    read ARCH
-+	fi
-+    fi;;
-+    yes) ARCH=$arch
-+esac
-+
-+# executable extension
-+
-+case $ARCH in
-+    win32) 
-+      EXE=".exe"
-+      DLLEXT=".dll";;
-+    *) EXE=""
-+       DLLEXT=".so"
-+esac
-+
-+# Is the source tree checked out from a recognised
-+# version control system ?
-+if test -e .svn/entries ; then 
-+    checkedout=svn
-+elif [ -d '{arch}' ]; then
-+    checkedout=gnuarch
-+elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
-+    checkedout=git
-+else
-+    checkedout=0
-+fi
-+
-+# make command
-+
-+MAKE=`which make`
-+if [ "$MAKE" != "" ]; then
-+  MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
-+  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
-+  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
-+  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-+      echo "You have GNU Make $MAKEVERSION. Good!"
-+  else
-+      OK="no"
-+      if [ -x ./make ]; then
-+	  MAKEVERSION=`./make -v | head -1`
-+	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
-+      fi
-+      if [ $OK = "no" ]; then
-+	  echo "GNU Make >= 3.81 is needed."
-+	  echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
-+	  echo "then locally installed on a Unix-style system by issuing:"
-+	  echo "  tar xzvf make-3.81.tar.gz"
-+	  echo "  cd make-3.81"
-+          echo "  ./configure"
-+          echo "  make"
-+          echo "  mv make .."
-+	  echo "  cd .."
-+	  echo "Restart then the configure script and later use ./make instead of make."
-+	  exit 1
-+      else
-+	  echo "You have locally installed GNU Make 3.81. Good!"
-+      fi
-+  fi
-+else
-+  echo "Cannot find GNU Make >= 3.81."
-+fi
-+
-+# Browser command
-+
-+if [ "$browser_spec" = "no" ]; then
-+    case $ARCH in
-+        win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
-+        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
-+    esac
-+fi
-+
-+if [ "$wwwcoq_spec" = "no" ]; then
-+    WWWCOQ="http://coq.inria.fr/"
-+fi
-+
-+#########################################
-+# Objective Caml programs
-+
-+case $camldir_spec in
-+    no) CAMLC=`which $bytecamlc`
-+	case "$CAMLC" in
-+	    "") echo "$bytecamlc is not present in your path!"
-+		echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
-+		read CAMLC
-+		
-+		case "$CAMLC" in
-+		    "") CAMLC=/usr/local/bin/$bytecamlc;;
-+		    */ocamlc|*/ocamlc.opt) true;;
-+		    */) CAMLC="${CAMLC}"$bytecamlc;;
-+		    *) CAMLC="${CAMLC}"/$bytecamlc;;
-+		esac
-+	esac
-+	CAMLBIN=`dirname "$CAMLC"`;;
-+    yes) CAMLC=$camldir/$bytecamlc
-+        
-+         CAMLBIN=`dirname "$CAMLC"`
-+	 bytecamlc="$CAMLC"
-+	 nativecamlc=$CAMLBIN/$nativecamlc
-+	 ocamlexec=$CAMLBIN/ocaml
-+	 ocamldepexec=$CAMLBIN/ocamldep
-+	 ocamldocexec=$CAMLBIN/ocamldoc
-+	 ocamllexexec=$CAMLBIN/ocamllex
-+	 ocamlyaccexec=$CAMLBIN/ocamlyacc
-+	 ocamlmktopexec=$CAMLBIN/ocamlmktop
-+	 ocamlmklibexec=$CAMLBIN/ocamlmklib
-+	 camlp4oexec=$CAMLBIN/camlp4o
-+esac
-+
-+if test ! -f "$CAMLC" ; then
-+    echo "I can not find the executable '$CAMLC'. Have you installed it?"
-+    echo "Configuration script failed!"
-+    exit 1
-+fi
-+
-+# Under Windows, OCaml only understands Windows filenames (C:\...)
-+case $ARCH in
-+    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
-+esac
-+
-+CAMLVERSION=`"$bytecamlc" -version`
-+
-+case $CAMLVERSION in
-+    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*)
-+	echo "Your version of Objective-Caml is $CAMLVERSION."
-+	if [ "$force_caml_version" = "yes" ]; then
-+	    echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
-+	else
-+	    echo "          You need Objective-Caml 3.10.2 or later."
-+	    echo "          Configuration script failed!"
-+	    exit 1
-+	fi;;
-+    ?*)
-+	CAMLP4COMPAT="-loc loc" 
-+	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-+    *)
-+	echo "I found the Objective-Caml compiler but cannot find its version number!"
-+	echo "Is it installed properly?"
-+	echo "Configuration script failed!"
-+	exit 1;;
-+esac
-+
-+CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
-+
-+# For coqmktop & bytecode compiler
-+
-+case $ARCH in
-+    win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
-+      CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
-+    *)
-+      CAMLLIB=`"$CAMLC" -where`
-+esac
-+
-+if [ "$coq_debug_flag" = "-g" ]; then
-+    case $CAMLTAG in
-+        OCAML31*)
-+            # Compilation debug flag
-+            coq_debug_flag_opt="-g"
-+            ;;
-+    esac
-+fi
-+
-+# Native dynlink
-+if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
-+    HASNATDYNLINK=true
-+else
-+    HASNATDYNLINK=false
-+fi
-+
-+case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
-+    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-+        NATDYNLINKFLAG=os5fixme;;
-+    #Possibly a problem on 10.6.0/10.6.1/10.6.2
-+    #May just be a 32 vs 64 problem for all 10.6.*
-+    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.*,3.11.*)
-+        if [ `getconf LONG_BIT` = "32" ]; then
-+	    # Still a problem for x86_32
-+            NATDYNLINKFLAG=os5fixme
-+        else
-+	    # Not a problem for x86_64
-+            NATDYNLINKFLAG=$HASNATDYNLINK
-+        fi;;
-+    *)
-+        NATDYNLINKFLAG=$HASNATDYNLINK;;
-+esac
-+
-+# Camlp4 / Camlp5 configuration
-+
-+if [ "$camlp5dir" != "" ]; then
-+    CAMLP4=camlp5
-+    CAMLP4LIB=$camlp5dir
-+    if [ ! -f $camlp5dir/camlp5.cma ]; then
-+	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
-+	echo "Configuration script failed!"
-+	exit 1
-+    fi
-+    camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-+else
-+    case $CAMLTAG in
-+        OCAML31*)
-+            if [ -x "${CAMLLIB}/camlp5" ]; then
-+                CAMLP4LIB=+camlp5
-+            elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
-+                CAMLP4LIB=+site-lib/camlp5
-+            else
-+	        echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
-+	        echo "Configuration script failed!"
-+	        exit 1
-+            fi
-+            CAMLP4=camlp5
-+            camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-+            ;;
-+        *)
-+            CAMLP4=camlp4
-+            CAMLP4LIB=+camlp4
-+            ;;
-+    esac
-+fi
-+
-+if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
-+    echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK"
-+    echo "(depending also on your ocaml version)."
-+    echo "Configuration script failed!"
-+    exit 1
-+fi
-+
-+
-+case $CAMLP4LIB in
-+    +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
-+    *)  FULLCAMLP4LIB=$CAMLP4LIB;;
-+esac
-+
-+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-+# (this should become configurable some day) 
-+CAMLP4BIN=${CAMLBIN}
-+
-+# do we have a native compiler: test of ocamlopt and its version
-+
-+if [ "$best_compiler" = "opt" ] ; then
-+  if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
-+      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-+      if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
-+	  case $CAMLOPTVERSION in
-+	      3.09.3|3.1?*) ;;
-+	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
-+		 best_compiler=byte
-+		 echo "only the bytecode version of Coq will be available."
-+	  esac
-+      elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
-+	  best_compiler=byte
-+	  echo "Cannot find native-code $CAMLP4,"
-+	  echo "only the bytecode version of Coq will be available."
-+      else
-+        if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-+	  echo "Native and bytecode compilers do not have the same version!"
-+        fi
-+        echo "You have native-code compilation. Good!"
-+      fi
-+  else
-+      best_compiler=byte
-+      echo "You have only bytecode compilation."
-+  fi
-+fi
-+
-+# OS dependent libraries
-+
-+case $ARCH in
-+  sun4*) OS=`uname -r`
-+	case $OS in
-+	   5*) OS="Sun Solaris $OS"
-+	       OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
-+	   *) OS="Sun OS $OS"
-+	      OSDEPLIBS="-cclib -lunix"
-+        esac;;
-+  alpha) OSDEPLIBS="-cclib -lunix";;
-+  win32) OS="Win32" 
-+	 OSDEPLIBS="-cclib -lunix"
-+	 cflags="-mno-cygwin $cflags";;
-+  *) OSDEPLIBS="-cclib -lunix"
-+esac
-+
-+# lablgtk2 and CoqIDE
-+
-+# -byte-only should imply -coqide byte, unless the user decides otherwise
-+
-+if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
-+    coqide_spec=yes
-+    COQIDE=byte
-+fi
-+
-+# Which coqide is asked ? which one is possible ?
-+
-+if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then 
-+    echo "CoqIde disabled as requested."
-+else
-+    case $lablgtkdir_spec in
-+	no) 
-+	    if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
-+		lablgtkdir=${CAMLLIB}/lablgtk2
-+	    elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
-+		lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
-+	    fi;;
-+	yes)
-+	    if [ ! -f "$lablgtkdir/glib.mli" ]; then
-+		echo "Incorrect LablGtk2 library (glib.mli not found)."
-+		echo "Configuration script failed!"
-+		exit 1
-+	    fi;;
-+    esac
-+    if [ "$lablgtkdir" = "" ]; then
-+	echo "LablGtk2 not found: CoqIde will not be available."
-+	COQIDE=no
-+    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
-+	echo "LablGtk2 found but too old: CoqIde will not be available."
-+	COQIDE=no;
-+    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then 
-+	echo "LablGtk2 found, bytecode CoqIde will be used as requested."
-+	COQIDE=byte
-+    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
-+	echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
-+	COQIDE=byte
-+    else 
-+	echo "LablGtk2 found, native threads: native CoqIde will be available."
-+	COQIDE=opt
-+    fi
-+fi
-+
-+case $COQIDE in
-+    byte|opt)
-+        case $lablgtkdir_spec in
-+            no)  LABLGTKLIB=+lablgtk2                   # Pour le message
-+                 LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
-+            yes) LABLGTKLIB="$lablgtkdir"               # Pour le message
-+                 LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
-+        esac;;
-+    no) LABLGTKINCLUDES="";;
-+esac
-+
-+# strip command
-+
-+case $ARCH in
-+    win32)
-+	# true -> strip : it exists under cygwin !
-+	STRIPCOMMAND="strip";; 
-+    *)
-+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
-+       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
-+    then
-+	STRIPCOMMAND="true"
-+    else
-+	STRIPCOMMAND="strip"
-+    fi
-+esac
-+
-+# mktexlsr
-+#MKTEXLSR=`which mktexlsr`
-+#case $MKTEXLSR in
-+#    "") MKTEXLSR=true;;
-+#esac
-+
-+# "
-+### Test if documentation can be compiled (latex, hevea)
-+
-+if test "$with_doc" = "all" 
-+then
-+    for cmd in "latex" "hevea" ; do
-+	if test ! -x "`which $cmd`"
-+	then 
-+	    echo "$cmd was not found; documentation will not be available"
-+	    with_doc=no
-+	    break
-+	fi
-+    done
-+fi
-+
-+###########################################
-+# bindir, libdir, mandir, docdir, etc.
-+
-+case $src_spec in
-+  no) COQTOP=${COQSRC}
-+esac
-+
-+# OCaml only understand Windows filenames (C:\...)
-+case $ARCH in
-+    win32) COQTOP=`cygpath -m ${COQTOP}`
-+esac
-+
-+case $ARCH in
-+  win32)
-+	 bindir_def='C:\coq\bin'
-+	 libdir_def='C:\coq\lib'
-+	 mandir_def='C:\coq\man'
-+	 docdir_def='C:\coq\doc'
-+	 emacslib_def='C:\coq\emacs'
-+         coqdocdir_def='C:\coq\latex';;
-+  *)
-+	 bindir_def=/usr/local/bin
-+	 libdir_def=/usr/local/lib/coq
-+	 mandir_def=/usr/local/man
-+	 docdir_def=/usr/local/share/doc/coq
-+	 emacslib_def=/usr/local/share/emacs/site-lisp
-+         coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
-+esac
-+
-+emacs_def=emacs
-+
-+case $bindir_spec/$prefix_spec/$local in
-+    yes/*/*) BINDIR=$bindir ;;
-+    */yes/*) BINDIR=$prefix/bin ;;
-+    */*/true) BINDIR=$COQTOP/bin ;;
-+    *) printf "Where should I install the Coq binaries [$bindir_def]? "
-+        read BINDIR
-+	case $BINDIR in
-+	    "") BINDIR=$bindir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $libdir_spec/$prefix_spec/$local in
-+    yes/*/*) LIBDIR=$libdir;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) LIBDIR=$prefix ;;
-+          *)  LIBDIR=$prefix/lib/coq ;;
-+        esac ;;
-+    */*/true) LIBDIR=$COQTOP ;;
-+    *)  printf "Where should I install the Coq library [$libdir_def]? "
-+        read LIBDIR
-+	case $LIBDIR in
-+	    "") LIBDIR=$libdir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $mandir_spec/$prefix_spec/$local in
-+    yes/*/*) MANDIR=$mandir;;
-+    */yes/*) MANDIR=$prefix/man ;;
-+    */*/true) MANDIR=$COQTOP/man ;;
-+    *)  printf "Where should I install the Coq man pages [$mandir_def]? "
-+        read MANDIR
-+	case $MANDIR in
-+	    "") MANDIR=$mandir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $docdir_spec/$prefix_spec/$local in
-+    yes/*/*) DOCDIR=$docdir; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+    */yes/*) DOCDIR=$prefix/share/doc/coq; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+    */*/true) DOCDIR=$COQTOP/doc; HTMLREFMANDIR=$DOCDIR/refman/html;;
-+    *)  printf "Where should I install the Coq documentation [$docdir_def]? "
-+        read DOCDIR
-+	case $DOCDIR in
-+	    "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $emacslib_spec/$prefix_spec/$local in
-+    yes/*/*) EMACSLIB=$emacslib;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) EMACSLIB=$prefix/emacs ;;
-+          *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
-+        esac ;;
-+    */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
-+    *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
-+        read EMACSLIB
-+	case $EMACSLIB in
-+	    "") EMACSLIB=$emacslib_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $coqdocdir_spec/$prefix_spec/$local in
-+    yes/*/*) COQDOCDIR=$coqdocdir;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) COQDOCDIR=$prefix/latex ;;
-+          *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
-+        esac ;;
-+    */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
-+    *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
-+        read COQDOCDIR
-+	case $COQDOCDIR in
-+	    "") COQDOCDIR=$coqdocdir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+# Determine if we enable -custom by default (Windows and MacOS)
-+CUSTOM_OS=no
-+if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
-+    CUSTOM_OS=yes
-+fi
-+
-+BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-+case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
-+    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
-+    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
-+    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
-+    *)
-+        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
-+        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
-+esac
-+case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
-+    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
-+    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
-+    *) COQTOOLSBYTEFLAGS="";;
-+esac
-+
-+# case $emacs_spec in
-+#     no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
-+#         read EMACS
-+	
-+# 	case $EMACS in
-+# 	    "") EMACS=$emacs_def;;
-+# 	    *) true;;
-+# 	esac;;
-+#     yes) EMACS=$emacs;;
-+# esac
-+
-+
-+
-+###########################################
-+# Summary of the configuration
-+
-+echo ""
-+echo "  Coq top directory                 : $COQTOP"
-+echo "  Architecture                      : $ARCH"
-+if test ! -z "$OS" ; then
-+  echo "  Operating system                  : $OS"
-+fi
-+echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
-+echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
-+echo "  OS dependent libraries            : $OSDEPLIBS"
-+echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
-+echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
-+echo "  Objective-Caml library in         : $CAMLLIB"
-+echo "  Camlp4 library in                 : $CAMLP4LIB"
-+if test "$best_compiler" = opt ; then
-+echo "  Native dynamic link support       : $HASNATDYNLINK"
-+fi
-+if test "$COQIDE" != "no"; then
-+echo "  Lablgtk2 library in               : $LABLGTKLIB"
-+fi
-+if test "$with_doc" = "all"; then
-+echo "  Documentation                     : All"
-+else
-+echo "  Documentation                     : None"
-+fi
-+echo "  CoqIde                            : $COQIDE"
-+echo "  Web browser                       : $BROWSER"
-+echo "  Coq web site                      : $WWWCOQ"
-+echo ""
-+
-+echo "  Paths for true installation:"
-+echo "    binaries      will be copied in $BINDIR"
-+echo "    library       will be copied in $LIBDIR"
-+echo "    man pages     will be copied in $MANDIR"
-+echo "    documentation will be copied in $DOCDIR"
-+echo "    emacs mode    will be copied in $EMACSLIB"
-+echo ""
-+
-+##################################################
-+# Building the $COQTOP/dev/ocamldebug-coq file
-+##################################################
-+
-+OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
-+
-+if test "$coq_debug_flag" = "-g" ; then
-+  rm -f $OCAMLDEBUGCOQ
-+  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-+      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-+      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-+      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
-+      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
-+  chmod a-w,a+x $OCAMLDEBUGCOQ
-+fi
-+
-+####################################################
-+# Fixing lablgtk types (before/after 2.6.0) 
-+####################################################
-+
-+if [ ! "$COQIDE" = "no" ]; then 
-+    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
-+       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
-+        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
-+       else
-+	cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
-+       fi
-+    else
-+	cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
-+    fi
-+fi  
-+
-+##############################################
-+# Creation of configuration files
-+##############################################
-+
-+mlconfig_file="$COQSRC/config/coq_config.ml"
-+config_file="$COQSRC/config/Makefile"
-+config_template="$COQSRC/config/Makefile.template"
-+
-+
-+### Warning !!
-+### After this line, be careful when using variables,
-+### since some of them (e.g. $COQSRC) will be escaped
-+
-+
-+# An escaped version of a variable
-+escape_var () {
-+"$ocamlexec" 2>&1 1>/dev/null <<EOF
-+  prerr_endline(String.escaped(Sys.getenv"$VAR"));;
-+EOF
-+}
-+
-+# Escaped version of browser command
-+export BROWSER
-+BROWSER=`VAR=BROWSER escape_var`
-+
-+# damned backslashes under M$Windows
-+case $ARCH in
-+    win32)
-+	COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
-+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
-+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
-+	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
-+	COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
-+	LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
-+	COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-+	COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-+	BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'`
-+	bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'`
-+	nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'`
-+	camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'`
-+    ;;
-+esac
-+
-+#####################################################
-+# Building the $COQTOP/config/coq_config.ml file
-+#####################################################
-+
-+rm -f "$mlconfig_file"
-+cat << END_OF_COQ_CONFIG > $mlconfig_file
-+(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-+
-+let local = $local
-+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-+let coqlib = "$LIBDIR"
-+let coqsrc = "$COQSRC"
-+let ocaml = "$ocamlexec"
-+let ocamlc = "$bytecamlc"
-+let ocamlopt = "$nativecamlc"
-+let ocamlmklib = "$ocamlmklibexec"
-+let ocamldep = "$ocamldepexec"
-+let ocamldoc = "$ocamldocexec"
-+let ocamlyacc = "$ocamlyaccexec"
-+let ocamllex = "$ocamllexexec"
-+let camlbin = "$CAMLBIN"
-+let camllib = "$CAMLLIB"
-+let camlp4 = "$CAMLP4"
-+let camlp4o = "$camlp4oexec"
-+let camlp4bin = "$CAMLP4BIN"
-+let camlp4lib = "$CAMLP4LIB"
-+let camlp4compat = "$CAMLP4COMPAT"
-+let coqideincl = "$LABLGTKINCLUDES"
-+let cflags = "$cflags"
-+let best = "$best_compiler"
-+let arch = "$ARCH"
-+let has_coqide = "$COQIDE"
-+let has_natdynlink = $HASNATDYNLINK
-+let natdynlinkflag = "$NATDYNLINKFLAG"
-+let osdeplibs = "$OSDEPLIBS"
-+let version = "$VERSION"
-+let caml_version = "$CAMLVERSION"
-+let date = "$DATE"
-+let compile_date = "$COMPILEDATE"
-+let vo_magic_number = $VOMAGIC
-+let state_magic_number = $STATEMAGIC
-+let exec_extension = "$EXE"
-+let with_geoproof = ref $with_geoproof
-+let browser = "$BROWSER"
-+let wwwcoq = "$WWWCOQ"
-+let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
-+let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-+let localwwwrefman = "file://$HTMLREFMANDIR/"
-+
-+END_OF_COQ_CONFIG
-+
-+# to be sure printf is found on windows when spaces occur in PATH variable
-+PRINTF=`which printf`
-+
-+# Subdirectories of theories/ added in coq_config.ml
-+subdirs () {
-+    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file")
-+}
-+
-+echo "let theories_dirs = [" >> "$mlconfig_file"
-+subdirs theories
-+echo "]" >> "$mlconfig_file"
-+
-+echo "let plugins_dirs = [" >> "$mlconfig_file"
-+subdirs plugins
-+echo "]" >> "$mlconfig_file"
-+
-+chmod a-w "$mlconfig_file"
-+
-+
-+###############################################
-+# Building the $COQTOP/config/Makefile file
-+###############################################
-+
-+rm -f "$config_file"
-+
-+sed -e "s|LOCALINSTALLATION|$local|" \
-+    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
-+    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
-+    -e "s|COQSRCDIRECTORY|$COQSRC|" \
-+    -e "s|COQVERSION|$VERSION|" \
-+    -e "s|BINDIRDIRECTORY|$BINDIR|" \
-+    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-+    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
-+    -e "s|MANDIRDIRECTORY|$MANDIR|" \
-+    -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
-+    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
-+    -e "s|EMACSCOMMAND|$EMACS|" \
-+    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
-+    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
-+    -e "s|ARCHITECTURE|$ARCH|" \
-+    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
-+    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-+    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
-+    -e "s|CAMLTAG|$CAMLTAG|" \
-+    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
-+    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-+    -e "s|CAMLP4TOOL|$camlp4oexec|" \
-+    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-+    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
-+    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
-+    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-+    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-+    -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
-+    -e "s|CCOMPILEFLAGS|$cflags|" \
-+    -e "s|BESTCOMPILER|$best_compiler|" \
-+    -e "s|DLLEXTENSION|$DLLEXT|" \
-+    -e "s|EXECUTEEXTENSION|$EXE|" \
-+    -e "s|BYTECAMLC|$bytecamlc|" \
-+    -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
-+    -e "s|NATIVECAMLC|$nativecamlc|" \
-+    -e "s|OCAMLEXEC|$ocamlexec|" \
-+    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
-+    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
-+    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
-+    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
-+    -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
-+    -e "s|CCEXEC|$gcc_exec|" \
-+    -e "s|AREXEC|$ar_exec|" \
-+    -e "s|RANLIBEXEC|$ranlib_exec|" \
-+    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
-+    -e "s|COQIDEOPT|$COQIDE|" \
-+    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
-+    -e "s|WITHDOCOPT|$with_doc|" \
-+    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
-+      "$config_template" > "$config_file"
-+
-+chmod a-w "$config_file"
-+
-+##################################################
-+# The end
-+####################################################
-+
-+echo "If anything in the above is wrong, please restart './configure'."
-+echo
-+echo "*Warning* To compile the system for a new architecture"
-+echo "          don't forget to do a 'make archclean' before './configure'."
-+
-+# $Id: configure 14833 2011-12-19 21:57:30Z notin $
diff --git a/pkgs/applications/science/logic/coq/configure.patch b/pkgs/applications/science/logic/coq/configure.patch
deleted file mode 100644
index aa38ce06e92b..000000000000
--- a/pkgs/applications/science/logic/coq/configure.patch
+++ /dev/null
@@ -1,11 +0,0 @@
-diff -Nuar coq-8.3pl3-orig/configure coq-8.3pl3/configure
---- coq-8.3pl3-orig/configure	2011-12-19 22:57:30.000000000 +0100
-+++ coq-8.3pl3/configure	2012-03-17 16:38:16.000000000 +0100
-@@ -395,7 +395,6 @@
- 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
- 	 ocamlmktopexec=$CAMLBIN/ocamlmktop
- 	 ocamlmklibexec=$CAMLBIN/ocamlmklib
--	 camlp4oexec=$CAMLBIN/camlp4o
- esac
- 
- if test ! -f "$CAMLC" ; then
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index dbfec66789a3..040d722f9410 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -24,9 +24,9 @@ let
    "8.7.2"     = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
    "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8";
    "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
+   "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
   }."${version}";
   coq-version = builtins.substring 0 3 version;
-  camlp5 = ocamlPackages.camlp5_strict;
   ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
   csdpPatch = if csdp != null then ''
     substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
@@ -36,8 +36,10 @@ self = stdenv.mkDerivation {
   name = "coq-${version}";
 
   passthru = {
-    inherit coq-version camlp5;
-    inherit (ocamlPackages) ocaml findlib num;
+    inherit coq-version;
+    inherit ocamlPackages;
+    # For compatibility
+    inherit (ocamlPackages) ocaml camlp5 findlib num;
     emacsBufferSetup = pkgs: ''
       ; Propagate coq paths to children
       (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
@@ -92,7 +94,7 @@ self = stdenv.mkDerivation {
   };
 
   nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib camlp5 ncurses ocamlPackages.num ]
+  buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ])
   ++ stdenv.lib.optional buildIde ocamlPackages.lablgtk;
 
   postPatch = ''
diff --git a/pkgs/applications/science/logic/coq/no-codesign.patch b/pkgs/applications/science/logic/coq/no-codesign.patch
deleted file mode 100644
index 0f917fbf56d4..000000000000
--- a/pkgs/applications/science/logic/coq/no-codesign.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-diff --git a/Makefile.build b/Makefile.build
-index 2963a3d..876479c 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -101,13 +101,8 @@ BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
- OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
- DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
- 
--ifeq ($(ARCH),Darwin)
--LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
--CODESIGN=codesign -s -
--else
- LINKMETADATA=
- CODESIGN=true
--endif
- 
- define bestocaml
- $(if $(OPT),\
-
diff --git a/pkgs/applications/science/logic/elan/default.nix b/pkgs/applications/science/logic/elan/default.nix
index 2b7cb9c30fae..f0b912c57fc5 100644
--- a/pkgs/applications/science/logic/elan/default.nix
+++ b/pkgs/applications/science/logic/elan/default.nix
@@ -2,15 +2,15 @@
 
 rustPlatform.buildRustPackage rec {
   name = "elan-${version}";
-  version = "0.5.0";
+  version = "0.7.1";
 
-  cargoSha256 = "01d3s47fjszxx8s5gr3haxq3kz3hswkrkr8x97wx8l4nfhm8ndd2";
+  cargoSha256 = "0vv7kr7rc3lvas7ngp5dp99ajjd5v8k5937ish7zqz1k4970q2f1";
 
   src = fetchFromGitHub {
     owner = "kha";
     repo = "elan";
     rev = "v${version}";
-    sha256 = "13zcqlyz0nwvd574llndrs7kvkznj6njljkq3v5j7kb3vndkj6i9";
+    sha256 = "0x5s1wm78yx5ci63wrmlkzm6k3281p33gn4dzw25k5s4vx0p9n24";
   };
 
   nativeBuildInputs = [ pkgconfig ];
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index a1779baf5f82..91be7dca1173 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,32 +1,37 @@
-{ stdenv, fetchFromGitHub, fetchpatch, ocaml, camlp5 }:
+{ stdenv, fetchFromGitHub, ocaml, num, camlp5 }:
 
 let
-  start_script = ''
-    #!/bin/sh
-    cd "$out/lib/hol_light"
-    exec ${ocaml}/bin/ocaml -I \`${camlp5}/bin/camlp5 -where\` -init make.ml
-  '';
+  load_num =
+    if num == null then "" else
+      ''
+        -I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \
+        -I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \
+        -I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \
+      '';
+
+  start_script =
+    ''
+      #!/bin/sh
+      cd $out/lib/hol_light
+      exec ${ocaml}/bin/ocaml \
+        -I \`${camlp5}/bin/camlp5 -where\` \
+        ${load_num} \
+        -init make.ml
+    '';
 in
 
 stdenv.mkDerivation {
-  name     = "hol_light-2017-07-06";
+  name     = "hol_light-2018-09-30";
 
   src = fetchFromGitHub {
     owner  = "jrh13";
     repo   = "hol-light";
-    rev    = "0ad8cbdb4de08a38dac600f352555e8454499faa";
-    sha256 = "0px9hl1b0mkyqv84j0si1zdq4066ffdrhzp27p2iah9l8ynbvpaq";
+    rev    = "27e09dd27834de46e917057710e9d8ded51a4c9f";
+    sha256 = "1p0rm08wnc2lsrh3xzhlq3zdhzqcv1lbqnkwx3aybrqhbg1ixc1d";
   };
 
   buildInputs = [ ocaml camlp5 ];
-
-  patches = [ (fetchpatch {
-      url = https://github.com/girving/hol-light/commit/f80524bad61fd6f6facaa42153b2e29d1eab4658.patch;
-      sha256 = "1563wp597vakhmsgg8940dpirzzfvvxqp75x3dnx20rvmi2n2xw0";
-    })
-  ];
-
-  postPatch = "cp pa_j_3.1x_{6,7}.xx.ml";
+  propagatedBuildInputs = [ num ];
 
   installPhase = ''
     mkdir -p "$out/lib/hol_light" "$out/bin"
diff --git a/pkgs/applications/science/logic/matita/130312.nix b/pkgs/applications/science/logic/matita/130312.nix
deleted file mode 100644
index 573b0ad7e4b5..000000000000
--- a/pkgs/applications/science/logic/matita/130312.nix
+++ /dev/null
@@ -1,65 +0,0 @@
-{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, ocaml_mysql, ocamlnet, ulex08, camlzip, ocaml_pcre, automake, autoconf }:
-
-let
-  version = "0.99.1pre130312";
-  pname = "matita";
-in
-
-stdenv.mkDerivation {
-  name = "${pname}-${version}";
-
-  src = fetchurl {
-    url = "http://matita.cs.unibo.it/sources/${pname}_130312.tar.gz";
-    sha256 = "13mjvvldv53dcdid6wmc6g8yn98xca26xq2rgq2jg700lqsni59s";
-  };
-
-  sourceRoot="${pname}-${version}";
-
-  unpackPhase = ''
-   mkdir $sourceRoot
-   tar -xvzf $src -C $sourceRoot
-   echo "source root is $sourceRoot"
-  '';
-
-  prePatch = ''
-   autoreconf -fvi
-  '';
-
-  buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk ocaml_mysql ocamlnet ulex08 camlzip ocaml_pcre automake autoconf];
-
-  postPatch = ''
-    BASH=$(type -tp bash)
-    substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace configure --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex"
-    substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex"
-    substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex"
-    substituteInPlace configure --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
-  '';
-
-  patches = [ ./configure_130312.patch ];
-
-  preConfigure = ''
-    # Setup for findlib.
-    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
-    RTDIR=$out/share/matita
-    export configureFlags="--with-runtime-dir=$RTDIR"
-  '';
-
-  postInstall = ''
-    mkdir -p $out/bin
-    ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
-  '';
-
-  meta = {
-    homepage = http://matita.cs.unibo.it/;
-    description = "Matita is an experimental, interactive theorem prover";
-    license = stdenv.lib.licenses.gpl2Plus;
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-    broken = true;
-  };
-}
diff --git a/pkgs/applications/science/logic/matita/Makefile.patch b/pkgs/applications/science/logic/matita/Makefile.patch
deleted file mode 100644
index 64c9a13f2d07..000000000000
--- a/pkgs/applications/science/logic/matita/Makefile.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- matita-0.5.8/Makefile	2009-12-01 18:21:00.000000000 -0500
-+++ matita-0.5.8/Makefile	2010-09-16 10:33:59.665461260 -0400
-@@ -38,7 +38,7 @@
- uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d))
- 
- rec@%:
--	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) DESTDIR=$(shell pwd)/$(DESTDIR)
-+	$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
- 
- # {{{ Distribution stuff
- 
diff --git a/pkgs/applications/science/logic/matita/configure.patch b/pkgs/applications/science/logic/matita/configure.patch
deleted file mode 100644
index 9a3bbbb13f52..000000000000
--- a/pkgs/applications/science/logic/matita/configure.patch
+++ /dev/null
@@ -1,36 +0,0 @@
---- zzz/matita-0.5.8/configure	2009-12-01 18:21:00.000000000 -0500
-+++ matita-0.5.8/configure	2010-09-07 19:57:29.732139550 -0400
-@@ -1895,6 +1895,7 @@
- # look for METAS dir
- 
- LIBSPATH="`pwd`/components"
-+OLDCAMLPATH="$OCAMLPATH"
- OCAMLPATH="$LIBSPATH/METAS"
- 
- # creating META.*
-@@ -1917,7 +1918,7 @@
- gdome2 \
- http \
- lablgtk2 \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- lablgtkmathview \
- mysql \
- netstring \
-@@ -1951,14 +1952,14 @@
- $FINDLIB_CREQUIRES \
- lablgtk2.glade \
- lablgtkmathview \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- helm-xmldiff \
- "
- for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
- do
-   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5
- $as_echo_n "checking for $r ocaml library... " >&6; }
--  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-+  if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-     { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
- $as_echo "yes" >&6; }
-   else
diff --git a/pkgs/applications/science/logic/matita/configure_130312.patch b/pkgs/applications/science/logic/matita/configure_130312.patch
deleted file mode 100644
index 255feec566bf..000000000000
--- a/pkgs/applications/science/logic/matita/configure_130312.patch
+++ /dev/null
@@ -1,35 +0,0 @@
---- matita/configure     2011-11-22 06:04:17.000000000 -0500
-+++ matita/configure     2011-11-24 11:43:11.584847938 -0500
-@@ -1905,6 +1905,7 @@
- # look for METAS dir
- 
- LIBSPATH="`pwd`/components"
-+OLDCAMLPATH="$OCAMLPATH"
- OCAMLPATH="$LIBSPATH/METAS"
- 
- # creating META.*
-@@ -1927,7 +1928,7 @@
- gdome2 \
- http \
- lablgtk2 \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- mysql \
- netstring \
- ulex08 \
-@@ -1953,13 +1954,13 @@
- FINDLIB_REQUIRES="\
- $FINDLIB_CREQUIRES \
- lablgtk2.glade \
--lablgtksourceview2.gtksourceview2 \
-+lablgtk2.gtksourceview \
- "
- for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
- do
-   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $r ocaml library" >&5
- $as_echo_n "checking for $r ocaml library... " >&6; }
--  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-+  if OCAMLPATH=$OCAMLPATH:$OLDCAMLPATH $OCAMLFIND query $r &> /dev/null; then
-     { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
- $as_echo "yes" >&6; }
-   else
diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix
deleted file mode 100644
index 5495f61bfd88..000000000000
--- a/pkgs/applications/science/logic/matita/default.nix
+++ /dev/null
@@ -1,52 +0,0 @@
-{stdenv, fetchurl, ocaml, findlib, gdome2, ocaml_expat, gmetadom, ocaml_http, lablgtk, lablgtkmathview, ocaml_mysql, ocaml_sqlite3, ocamlnet, ulex08, camlzip, ocaml_pcre }:
-
-let
-  version = "0.5.8";
-  pname = "matita";
-in
-
-stdenv.mkDerivation {
-  name = "${pname}-${version}";
-
-  src = fetchurl {
-    url = "http://matita.cs.unibo.it/FILES/${pname}-${version}.orig.tar.gz";
-    sha256 = "04sxklfak71khy1f07ks5c6163jbpxv6fmaw03fx8gwwlvpmzglh";
-  };
-
-  buildInputs = [ocaml findlib gdome2 ocaml_expat gmetadom ocaml_http lablgtk lablgtkmathview ocaml_mysql ocaml_sqlite3 ocamlnet ulex08 camlzip ocaml_pcre ];
-
-  postPatch = ''
-    BASH=$(type -tp bash)
-    substituteInPlace components/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace matita/Makefile --replace "SHELL=/bin/bash" "SHELL=$BASH"
-    substituteInPlace configure --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-content_pres.src --replace "ulex08" "ulex"
-    substituteInPlace components/content_pres/Makefile --replace "ulex08" "ulex"
-    substituteInPlace components/METAS/meta.helm-grafite_parser.src --replace "ulex08" "ulex"
-    substituteInPlace components/grafite_parser/Makefile --replace "ulex08" "ulex"
-    substituteInPlace configure --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-getter.src --replace "zip" "camlzip"
-    substituteInPlace components/METAS/meta.helm-xml.src --replace "zip" "camlzip"
-  '';
-
-  patches = [ ./configure.patch ./Makefile.patch ];
-
-  preConfigure = ''
-    # Setup for findlib.
-    OCAMLPATH=$(pwd)/components/METAS:$OCAMLPATH
-    RTDIR=$out/share/matita
-    export configureFlags="--with-runtime-dir=$RTDIR"
-  '';
-
-  postInstall = ''
-    mkdir -p $out/bin
-    ln -vs $RTDIR/matita $RTDIR/matitac $RTDIR/matitaclean $RTDIR/matitadep $RTDIR/matitawiki $out/bin
-  '';
-
-  meta = {
-    homepage = http://matita.cs.unibo.it/;
-    description = "Experimental, interactive theorem prover";
-    license = stdenv.lib.licenses.gpl2Plus;
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-  };
-}
diff --git a/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix
index 01dfc35f6e0d..1f6620a2872d 100644
--- a/pkgs/applications/science/logic/prooftree/default.nix
+++ b/pkgs/applications/science/logic/prooftree/default.nix
@@ -1,21 +1,22 @@
-{stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }:
 
-stdenv.mkDerivation (rec {
+stdenv.mkDerivation rec {
   name = "prooftree-${version}";
-  version = "0.12";
+  version = "0.13";
 
   src = fetchurl {
     url = "https://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz";
-    sha256 = "08yp66j05pdkdpv9xkfqymqy82mir5xbwfh9mkzhh219xkps4b4m";
+    sha256 = "0z1z4wqbqwgppkh2bm89fgy07a0y2m6g4lvcyzs09sm1ysklk2dh";
   };
 
   nativeBuildInputs = [ pkgconfig ];
-  buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
+  buildInputs = [ ncurses ] ++ (with ocamlPackages; [
+    ocaml findlib camlp5 lablgtk ]);
 
   dontAddPrefix = true;
   configureFlags = [ "--prefix" "$(out)" ];
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "A program for proof-tree visualization";
     longDescription = ''
       Prooftree is a program for proof-tree visualization during interactive
@@ -35,7 +36,8 @@ stdenv.mkDerivation (rec {
       shift-click).
     '';
     homepage = http://askra.de/software/prooftree;
-    platforms = stdenv.lib.platforms.unix;
-    maintainers = [ stdenv.lib.maintainers.jwiegley ];
+    platforms = platforms.unix;
+    maintainers = [ maintainers.jwiegley ];
+    license = licenses.gpl3;
   };
-})
+}
diff --git a/pkgs/applications/science/logic/symbiyosys/default.nix b/pkgs/applications/science/logic/symbiyosys/default.nix
index 946f65d944b3..e21c274370c8 100644
--- a/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   name = "symbiyosys-${version}";
-  version = "2018.07.26";
+  version = "2018.09.12";
 
   src = fetchFromGitHub {
     owner  = "yosyshq";
     repo   = "symbiyosys";
-    rev    = "2fef25f93dd1cb5137a08e71f507e3eee8100fb1";
-    sha256 = "103fga0n11h4n2q346xyz3k0615d9lgx2b8sqr1pwn2hx26kchav";
+    rev    = "e90bcb588e97118af0cdba23fae562fb0efbf294";
+    sha256 = "16nlimpdc3g6lghwqpyirgrr1d9mgk4wg3c06fvglzaicvjixnfr";
   };
 
   buildInputs = [ python3 yosys ];
diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 4efc384ed227..9056eab71ea3 100644
--- a/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -31,7 +31,8 @@ let
   '';
 
   tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
-    patchPhase = replaceSymlinks;
+    postPatch = replaceSymlinks;
+    patches = [ ./ghc-8.4-support-utils.patch ];
     libraryHaskellDepends = with haskellPackages; [
       base base64-bytestring binary blaze-builder bytestring containers
       deepseq dlist fclabels mtl pretty safe SHA syb time transformers
@@ -39,7 +40,8 @@ let
   });
 
   tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // {
-    patchPhase = replaceSymlinks;
+    postPatch = replaceSymlinks;
+    patches = [ ./ghc-8.4-support-term.patch ];
     libraryHaskellDepends = (with haskellPackages; [
       attoparsec base binary bytestring containers deepseq dlist HUnit
       mtl process safe
@@ -47,7 +49,8 @@ let
   });
 
   tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // {
-    patchPhase = replaceSymlinks;
+    postPatch = replaceSymlinks;
+    patches = [ ./ghc-8.4-support-theory.patch ];
     doHaddock = false; # broken
     libraryHaskellDepends = (with haskellPackages; [
       aeson aeson-pretty base binary bytestring containers deepseq dlist
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch
new file mode 100644
index 000000000000..f93919faf54e
--- /dev/null
+++ b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch
@@ -0,0 +1,109 @@
+From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
+From: Felix Yan <felixonmars@archlinux.org>
+Date: Fri, 18 May 2018 16:24:41 +0800
+Subject: [PATCH] GHC 8.4 support
+
+---
+ src/Term/Maude/Signature.hs          |  8 ++--
+ src/Term/Rewriting/Definitions.hs    | 23 ++++++----
+ src/Term/Unification.hs              |  4 +-
+ 11 files changed, 79 insertions(+), 48 deletions(-)
+
+diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs
+index 98c25d9f..1a4ce82f 100644
+--- a/src/Term/Maude/Signature.hs
++++ b/src/Term/Maude/Signature.hs
+@@ -104,9 +104,9 @@ maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,enableXor,enableDiff=_,stF
+           `S.union` dhReducibleFunSig `S.union` bpReducibleFunSig `S.union` xorReducibleFunSig
+ 
+ -- | A monoid instance to combine maude signatures.
+-instance Monoid MaudeSig where
+-    (MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _) `mappend`
+-      (MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _) =
++instance Semigroup MaudeSig where
++    MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _ <>
++      MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _ =
+           maudeSig (mempty {enableDH=dh1||dh2
+                            ,enableBP=bp1||bp2
+                            ,enableMSet=mset1||mset2
+@@ -114,6 +114,8 @@ instance Monoid MaudeSig where
+                            ,enableDiff=diff1||diff2
+                            ,stFunSyms=S.union stFunSyms1 stFunSyms2
+                            ,stRules=S.union stRules1 stRules2})
++
++instance Monoid MaudeSig where
+     mempty = MaudeSig False False False False False S.empty S.empty S.empty S.empty
+ 
+ -- | Non-AC function symbols.
+diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs
+index bd942b6a..18562e4e 100644
+--- a/src/Term/Rewriting/Definitions.hs
++++ b/src/Term/Rewriting/Definitions.hs
+@@ -44,10 +44,12 @@ evalEqual (Equal l r) = l == r
+ instance Functor Equal where
+     fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs)
+ 
++instance Semigroup a => Semigroup (Equal a) where
++    (Equal l1 r1) <> (Equal l2 r2) =
++        Equal (l1 <> l2) (r1 <> r2)
++
+ instance Monoid a => Monoid (Equal a) where
+     mempty                                = Equal mempty mempty
+-    (Equal l1 r1) `mappend` (Equal l2 r2) =
+-        Equal (l1 `mappend` l2) (r1 `mappend` r2)
+ 
+ instance Foldable Equal where
+     foldMap f (Equal l r) = f l `mappend` f r
+@@ -104,14 +106,15 @@ instance Functor Match where
+     fmap _ NoMatch             = NoMatch
+     fmap f (DelayedMatches ms) = DelayedMatches (fmap (f *** f) ms)
+ 
++instance Semigroup (Match a) where
++    NoMatch            <> _                  = NoMatch
++    _                  <> NoMatch            = NoMatch
++    DelayedMatches ms1 <> DelayedMatches ms2 =
++        DelayedMatches (ms1 <> ms2)
++
+ instance Monoid (Match a) where
+     mempty = DelayedMatches []
+ 
+-    NoMatch            `mappend` _                  = NoMatch
+-    _                  `mappend` NoMatch            = NoMatch
+-    DelayedMatches ms1 `mappend` DelayedMatches ms2 =
+-        DelayedMatches (ms1 `mappend` ms2)
+-
+ 
+ instance Foldable Match where
+     foldMap _ NoMatch             = mempty
+@@ -136,10 +139,12 @@ data RRule a = RRule a a
+ instance Functor RRule where
+     fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs)
+ 
++instance Monoid a => Semigroup (RRule a) where
++    (RRule l1 r1) <> (RRule l2 r2) =
++        RRule (l1 <> l2) (r1 <> r2)
++
+ instance Monoid a => Monoid (RRule a) where
+     mempty                                = RRule mempty mempty
+-    (RRule l1 r1) `mappend` (RRule l2 r2) =
+-        RRule (l1 `mappend` l2) (r1 `mappend` r2)
+ 
+ instance Foldable RRule where
+     foldMap f (RRule l r) = f l `mappend` f r
+diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs
+index e1de0163..7ce6bb41 100644
+--- a/src/Term/Unification.hs
++++ b/src/Term/Unification.hs
+@@ -265,9 +265,11 @@ unifyRaw l0 r0 = do
+ 
+ data MatchFailure = NoMatcher | ACProblem
+ 
++instance Semigroup MatchFailure where
++  _ <> _ = NoMatcher
++
+ instance Monoid MatchFailure where
+   mempty = NoMatcher
+-  mappend _ _ = NoMatcher
+ 
+ -- | Ensure that the computed substitution @sigma@ satisfies
+ -- @t ==_AC apply sigma p@ after the delayed equations are solved.
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
new file mode 100644
index 000000000000..f7393e37f1b2
--- /dev/null
+++ b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
@@ -0,0 +1,130 @@
+From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
+From: Felix Yan <felixonmars@archlinux.org>
+Date: Fri, 18 May 2018 16:24:41 +0800
+Subject: [PATCH] GHC 8.4 support
+
+---
+ src/Theory/Proof.hs                | 43 +++++++++++--------
+ 11 files changed, 79 insertions(+), 48 deletions(-)
+
+diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs
+index ddbc965a..6daadd0d 100644
+--- a/src/Theory/Constraint/Solver/Reduction.hs
++++ b/src/Theory/Constraint/Solver/Reduction.hs
+@@ -139,13 +139,14 @@ execReduction m ctxt se fs =
+ data ChangeIndicator = Unchanged | Changed
+        deriving( Eq, Ord, Show )
+ 
++instance Semigroup ChangeIndicator where
++    Changed   <> _         = Changed
++    _         <> Changed   = Changed
++    Unchanged <> Unchanged = Unchanged
++
+ instance Monoid ChangeIndicator where
+     mempty = Unchanged
+ 
+-    Changed   `mappend` _         = Changed
+-    _         `mappend` Changed   = Changed
+-    Unchanged `mappend` Unchanged = Unchanged
+-
+ -- | Return 'True' iff there was a change.
+ wasChanged :: ChangeIndicator -> Bool
+ wasChanged Changed   = True
+diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs
+index f98fc7c2..2aac8ce2 100644
+--- a/src/Theory/Constraint/System/Guarded.hs
++++ b/src/Theory/Constraint/System/Guarded.hs
+@@ -435,7 +435,7 @@ gall ss atos gf               = GGuarded All ss atos gf
+ 
+ -- | Local newtype to avoid orphan instance.
+ newtype ErrorDoc d = ErrorDoc { unErrorDoc :: d }
+-    deriving( Monoid, NFData, Document, HighlightDocument )
++    deriving( Monoid, Semigroup, NFData, Document, HighlightDocument )
+ 
+ -- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is
+ -- equivalent to @fm@ under the assumption that this is possible.
+diff --git a/src/Theory/Proof.hs b/src/Theory/Proof.hs
+index 74fb77b1..7971b9fc 100644
+--- a/src/Theory/Proof.hs
++++ b/src/Theory/Proof.hs
+@@ -388,17 +388,19 @@ data ProofStatus =
+        | TraceFound         -- ^ There is an annotated solved step
+     deriving ( Show, Generic, NFData, Binary )
+ 
++instance Semigroup ProofStatus where
++    TraceFound <> _                        = TraceFound
++    _ <> TraceFound                        = TraceFound
++    IncompleteProof <> _                   = IncompleteProof
++    _ <> IncompleteProof                   = IncompleteProof
++    _ <> CompleteProof                     = CompleteProof
++    CompleteProof <> _                     = CompleteProof
++    UndeterminedProof <> UndeterminedProof = UndeterminedProof
++
++
+ instance Monoid ProofStatus where
+     mempty = CompleteProof
+ 
+-    mappend TraceFound _                        = TraceFound
+-    mappend _ TraceFound                        = TraceFound
+-    mappend IncompleteProof _                   = IncompleteProof
+-    mappend _ IncompleteProof                   = IncompleteProof
+-    mappend _ CompleteProof                     = CompleteProof
+-    mappend CompleteProof _                     = CompleteProof
+-    mappend UndeterminedProof UndeterminedProof = UndeterminedProof
+-
+ -- | The status of a 'ProofStep'.
+ proofStepStatus :: ProofStep (Maybe a) -> ProofStatus
+ proofStepStatus (ProofStep _         Nothing ) = UndeterminedProof
+@@ -560,10 +562,12 @@ newtype Prover =  Prover
+               -> Maybe IncrementalProof    -- resulting proof
+           }
+ 
++instance Semigroup Prover where
++    p1 <> p2 = Prover $ \ctxt d se ->
++        runProver p1 ctxt d se >=> runProver p2 ctxt d se
++
+ instance Monoid Prover where
+     mempty          = Prover $ \_  _ _ -> Just
+-    p1 `mappend` p2 = Prover $ \ctxt d se ->
+-        runProver p1 ctxt d se >=> runProver p2 ctxt d se
+ 
+ -- | Provers whose sequencing is handled via the 'Monoid' instance.
+ --
+@@ -579,10 +583,12 @@ newtype DiffProver =  DiffProver
+               -> Maybe IncrementalDiffProof    -- resulting proof
+           }
+ 
++instance Semigroup DiffProver where
++    p1 <> p2 = DiffProver $ \ctxt d se ->
++        runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
++
+ instance Monoid DiffProver where
+     mempty          = DiffProver $ \_  _ _ -> Just
+-    p1 `mappend` p2 = DiffProver $ \ctxt d se ->
+-        runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
+ 
+ -- | Map the proof generated by the prover.
+ mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> Prover
+@@ -784,15 +790,16 @@ runAutoDiffProver (AutoProver heuristic bound cut) =
+ -- | The result of one pass of iterative deepening.
+ data IterDeepRes = NoSolution | MaybeNoSolution | Solution ProofPath
+ 
++instance Semigroup IterDeepRes where
++    x@(Solution _)   <> _                = x
++    _                <> y@(Solution _)   = y
++    MaybeNoSolution  <> _                = MaybeNoSolution
++    _                <> MaybeNoSolution  = MaybeNoSolution
++    NoSolution       <> NoSolution       = NoSolution
++
+ instance Monoid IterDeepRes where
+     mempty = NoSolution
+ 
+-    x@(Solution _)   `mappend` _                = x
+-    _                `mappend` y@(Solution _)   = y
+-    MaybeNoSolution  `mappend` _                = MaybeNoSolution
+-    _                `mappend` MaybeNoSolution  = MaybeNoSolution
+-    NoSolution       `mappend` NoSolution       = NoSolution
+-
+ -- | @cutOnSolvedDFS prf@ removes all other cases if an attack is found. The
+ -- attack search is performed using a parallel DFS traversal with iterative
+ -- deepening.
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch
new file mode 100644
index 000000000000..d6cd6d73f99e
--- /dev/null
+++ b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch
@@ -0,0 +1,140 @@
+From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
+From: Felix Yan <felixonmars@archlinux.org>
+Date: Fri, 18 May 2018 16:24:41 +0800
+Subject: [PATCH] GHC 8.4 support
+
+---
+ src/Extension/Data/Bounded.hs       | 10 ++++-
+ src/Extension/Data/Monoid.hs        | 14 +++---
+ src/Logic/Connectives.hs            |  4 +-
+ src/Text/PrettyPrint/Class.hs       |  4 +-
+ src/Text/PrettyPrint/Html.hs        |  6 ++-
+ 11 files changed, 79 insertions(+), 48 deletions(-)
+
+
+diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs
+index 5f166006..f416a44c 100644
+--- a/src/Extension/Data/Bounded.hs
++++ b/src/Extension/Data/Bounded.hs
+@@ -11,19 +11,25 @@ module Extension.Data.Bounded (
+   ) where
+ 
+ -- import Data.Monoid
++import Data.Semigroup
+ 
+ -- | A newtype wrapper for a monoid of the maximum of a bounded type.
+ newtype BoundedMax a = BoundedMax {getBoundedMax :: a}
+     deriving( Eq, Ord, Show )
+ 
++instance (Ord a, Bounded a) => Semigroup (BoundedMax a) where
++    BoundedMax x <> BoundedMax y = BoundedMax (max x y)
++
+ instance (Ord a, Bounded a) => Monoid (BoundedMax a) where
+     mempty                                  = BoundedMax minBound
+-    (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y)
++    mappend = (<>)
+ 
+ -- | A newtype wrapper for a monoid of the minimum of a bounded type.
+ newtype BoundedMin a = BoundedMin {getBoundedMin :: a}
+     deriving( Eq, Ord, Show )
+ 
++instance (Ord a, Bounded a) => Semigroup (BoundedMin a) where
++    BoundedMin x <> BoundedMin y = BoundedMin (min x y)
++
+ instance (Ord a, Bounded a) => Monoid (BoundedMin a) where
+     mempty                                  = BoundedMin maxBound
+-    (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y)
+\ No newline at end of file
+diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs
+index 83655c34..9ce2f91b 100644
+--- a/src/Extension/Data/Monoid.hs
++++ b/src/Extension/Data/Monoid.hs
+@@ -18,6 +18,7 @@ module Extension.Data.Monoid (
+   ) where
+ 
+ import Data.Monoid
++import Data.Semigroup
+ 
+ #if __GLASGOW_HASKELL__ < 704
+ 
+@@ -38,10 +39,13 @@ newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) }
+ minMaxSingleton :: a -> MinMax a
+ minMaxSingleton x = MinMax (Just (x, x))
+ 
++instance Ord a => Semigroup (MinMax a) where
++    MinMax Nothing             <> y                          = y
++    x                          <> MinMax Nothing             = x
++    MinMax (Just (xMin, xMax)) <> MinMax (Just (yMin, yMax)) =
++       MinMax (Just (min xMin yMin, max xMax yMax))
++
++
+ instance Ord a => Monoid (MinMax a) where
+     mempty = MinMax Nothing
+-
+-    MinMax Nothing             `mappend` y                          = y
+-    x                          `mappend` MinMax Nothing             = x
+-    MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) =
+-       MinMax (Just (min xMin yMin, max xMax yMax))
++    mappend = (<>)
+diff --git a/src/Logic/Connectives.hs b/src/Logic/Connectives.hs
+index 2e441172..7206cc2c 100644
+--- a/src/Logic/Connectives.hs
++++ b/src/Logic/Connectives.hs
+@@ -23,12 +23,12 @@ import Control.DeepSeq
+ 
+ -- | A conjunction of atoms of type a.
+ newtype Conj a = Conj { getConj :: [a] }
+-  deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
++  deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
+             Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
+ 
+ -- | A disjunction of atoms of type a.
+ newtype Disj a = Disj { getDisj :: [a] }
+-  deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
++  deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
+             Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
+ 
+ instance MonadDisj Disj where
+diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs
+index f5eb42fe..13be6515 100644
+--- a/src/Text/PrettyPrint/Class.hs
++++ b/src/Text/PrettyPrint/Class.hs
+@@ -187,9 +187,11 @@ instance Document Doc where
+   nest i (Doc d) = Doc $ P.nest i d
+   caseEmptyDoc yes no (Doc d) = if P.isEmpty d then yes else no
+ 
++instance Semigroup Doc where
++    Doc d1 <> Doc d2 = Doc $ (P.<>) d1 d2
++
+ instance Monoid Doc where
+     mempty = Doc $ P.empty
+-    mappend (Doc d1) (Doc d2) = Doc $ (P.<>) d1 d2
+   
+ ------------------------------------------------------------------------------
+ -- Additional combinators
+diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs
+index 3de5e307..10103eb7 100644
+--- a/src/Text/PrettyPrint/Html.hs
++++ b/src/Text/PrettyPrint/Html.hs
+@@ -90,7 +90,7 @@ attribute (key,value) = " " ++ key ++ "=\"" ++ escapeHtmlEntities value ++ "\""
+ 
+ -- | A 'Document' transformer that adds proper HTML escaping.
+ newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }
+-    deriving( Monoid )
++    deriving( Monoid, Semigroup )
+ 
+ -- | Wrap a document such that HTML markup can be added without disturbing the
+ -- layout.
+@@ -182,9 +182,11 @@ getNoHtmlDoc = runIdentity . unNoHtmlDoc
+ instance NFData d => NFData (NoHtmlDoc d) where
+     rnf = rnf . getNoHtmlDoc
+ 
++instance Semigroup d => Semigroup (NoHtmlDoc d) where
++  (<>) = liftA2 (<>)
++
+ instance Monoid d => Monoid (NoHtmlDoc d) where
+   mempty = pure mempty
+-  mappend = liftA2 mappend
+ 
+ instance Document d => Document (NoHtmlDoc d) where
+   char = pure . char
diff --git a/pkgs/applications/science/logic/tlaplus/toolbox.nix b/pkgs/applications/science/logic/tlaplus/toolbox.nix
index 342d91cf5825..f1116a27c0be 100644
--- a/pkgs/applications/science/logic/tlaplus/toolbox.nix
+++ b/pkgs/applications/science/logic/tlaplus/toolbox.nix
@@ -44,7 +44,7 @@ in stdenv.mkDerivation {
       --run "set -x; cd $out/toolbox" \
       --add-flags "-data ~/.tla-toolbox" \
       --prefix PATH : "${jre}/bin" \
-      --prefix LD_LIBRARY_PATH : "${swt}/lib:${gtk}/lib:${libXtst}/lib:${glib}/lib"
+      --prefix LD_LIBRARY_PATH : "${lib.makeLibraryPath [ swt gtk libXtst glib ]}"
 
     echo -e "\nCreating TLA Toolbox icons..."
     pushd "$src"
diff --git a/pkgs/applications/science/logic/tptp/default.nix b/pkgs/applications/science/logic/tptp/default.nix
index a1d613e6295e..f3c4f22eae36 100644
--- a/pkgs/applications/science/logic/tptp/default.nix
+++ b/pkgs/applications/science/logic/tptp/default.nix
@@ -12,7 +12,8 @@ stdenv.mkDerivation rec {
     sha256 = "0slqbqv4y43wz6wnh72s4n540ssapah0d12mndi0c7xr04kf2v2d";
   };
 
-  buildInputs = [ tcsh yap perl patchelf ];
+  nativeBuildInputs = [ patchelf ];
+  buildInputs = [ tcsh yap perl ];
 
   installPhase = ''
     sharedir=$out/share/tptp
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index 1ccc365498ce..58609e856c3b 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   name    = "why3-${version}";
-  version = "1.0.0";
+  version = "1.1.0";
 
   src = fetchurl {
-    url    = https://gforge.inria.fr/frs/download.php/file/37604/why3-1.0.0.tar.gz;
-    sha256 = "18h00diw1c051v7ya0lv09ns5630qi9savwffx0652mcc4b4qpxn";
+    url    = https://gforge.inria.fr/frs/download.php/file/37767/why3-1.1.0.tar.gz;
+    sha256 = "199ziq8mv3r24y3dd1n2r8k2gy09p7kdyyhkg9qn1vzfd2fxwzc1";
   };
 
   buildInputs = (with ocamlPackages; [
diff --git a/pkgs/applications/science/math/almonds/default.nix b/pkgs/applications/science/math/almonds/default.nix
index 96613f4e38a6..b5d9632c551d 100644
--- a/pkgs/applications/science/math/almonds/default.nix
+++ b/pkgs/applications/science/math/almonds/default.nix
@@ -20,8 +20,7 @@ with python3.pkgs; buildPythonApplication rec {
   meta = with stdenv.lib; {
     description = "Terminal Mandelbrot fractal viewer";
     homepage = https://github.com/Tenchi2xh/Almonds;
-    # No license has been specified
-    license = licenses.unfree;
+    license = licenses.mit;
     maintainers = with maintainers; [ infinisil ];
   };
 }
diff --git a/pkgs/applications/science/math/calc/default.nix b/pkgs/applications/science/math/calc/default.nix
index 9d95960bde27..ff6b2d0ad2d1 100644
--- a/pkgs/applications/science/math/calc/default.nix
+++ b/pkgs/applications/science/math/calc/default.nix
@@ -3,14 +3,14 @@
 
 stdenv.mkDerivation rec {
   name = "calc-${version}";
-  version = "2.12.6.6";
+  version = "2.12.6.8";
 
   src = fetchurl {
     urls = [
       "https://github.com/lcn2/calc/releases/download/${version}/${name}.tar.bz2"
       "http://www.isthe.com/chongo/src/calc/${name}.tar.bz2"
     ];
-    sha256 = "03sg1xhin6qsrz82scf96mmzw8lz1yj68rhj4p4npp4s0fawc9d5";
+    sha256 = "144am0pra3hh7635fmi7kqynba8z246dx1dzclm9qx965p3xb4hb";
   };
 
   patchPhase = ''
diff --git a/pkgs/applications/science/math/gmsh/default.nix b/pkgs/applications/science/math/gmsh/default.nix
index 7bc8729c3fe5..525fc5f1dc26 100644
--- a/pkgs/applications/science/math/gmsh/default.nix
+++ b/pkgs/applications/science/math/gmsh/default.nix
@@ -1,14 +1,14 @@
 { stdenv, fetchurl, cmake, blas, liblapack, gfortran, gmm, fltk, libjpeg
 , zlib, libGLU_combined, libGLU, xorg }:
 
-let version = "4.0.0"; in
+let version = "4.0.2"; in
 
 stdenv.mkDerivation {
   name = "gmsh-${version}";
 
   src = fetchurl {
     url = "http://gmsh.info/src/gmsh-${version}-source.tgz";
-    sha256 = "0pqm0ippj0j07919hld3f3rgq0p1x4j32fxb2m1nyp226zx8l37v";
+    sha256 = "03aw3sbz4x998rk29az7mgm0mrdb6614aqnppg81p5jkh5097jgk";
   };
 
   # The original CMakeLists tries to use some version of the Lapack lib
diff --git a/pkgs/applications/science/math/mxnet/default.nix b/pkgs/applications/science/math/mxnet/default.nix
index ce9c214b3f0c..990d3f1a5d59 100644
--- a/pkgs/applications/science/math/mxnet/default.nix
+++ b/pkgs/applications/science/math/mxnet/default.nix
@@ -1,5 +1,5 @@
-{ stdenv, lib, fetchgit, cmake
-, opencv, gtest, openblas, liblapack
+{ stdenv, lib, fetchurl, bash, cmake
+, opencv, gtest, openblas, liblapack, perl
 , cudaSupport ? false, cudatoolkit, nvidia_x11
 , cudnnSupport ? false, cudnn
 }:
@@ -8,16 +8,17 @@ assert cudnnSupport -> cudaSupport;
 
 stdenv.mkDerivation rec {
   name = "mxnet-${version}";
-  version = "1.1.0";
-
-  # Submodules needed
-  src = fetchgit {
-    url = "https://github.com/apache/incubator-mxnet";
-    rev = "refs/tags/${version}";
-    sha256 = "1qgns0c70a1gfyil96h17ms736nwdkp9kv496gvs9pkzqzvr6cpz";
+  version = "1.2.1";
+
+  # Fetching from git does not work at the time (1.2.1) due to an
+  # incorrect hash in one of the submodules. The provided tarballs
+  # contain all necessary sources.
+  src = fetchurl {
+    url = "https://github.com/apache/incubator-mxnet/releases/download/${version}/apache-mxnet-src-${version}-incubating.tar.gz";
+    sha256 = "053zbdgs4j8l79ipdz461zc7wyfbfcflmi5bw7lj2q08zm1glnb2";
   };
 
-  nativeBuildInputs = [ cmake ];
+  nativeBuildInputs = [ cmake perl ];
 
   buildInputs = [ opencv gtest openblas liblapack ]
               ++ lib.optionals cudaSupport [ cudatoolkit nvidia_x11 ]
@@ -30,9 +31,17 @@ stdenv.mkDerivation rec {
     ] else [ "-DUSE_CUDA=OFF" ])
     ++ lib.optional (!cudnnSupport) "-DUSE_CUDNN=OFF";
 
-  installPhase = ''
-    install -Dm755 libmxnet.so $out/lib/libmxnet.so
-    cp -r ../include $out
+  postPatch = ''
+    substituteInPlace 3rdparty/mkldnn/tests/CMakeLists.txt \
+      --replace "/bin/bash" "${bash}/bin/bash"
+
+    # Build against the system version of OpenMP. 
+    # https://github.com/apache/incubator-mxnet/pull/12160
+    rm -rf 3rdparty/openmp
+  '';
+
+  postInstall = ''
+    rm "$out"/lib/*.a
   '';
 
   enableParallelBuilding = true;
diff --git a/pkgs/applications/science/math/nauty/default.nix b/pkgs/applications/science/math/nauty/default.nix
index d7b4707420be..9639376fbda3 100644
--- a/pkgs/applications/science/math/nauty/default.nix
+++ b/pkgs/applications/science/math/nauty/default.nix
@@ -1,10 +1,10 @@
 {stdenv, fetchurl}:
 stdenv.mkDerivation rec {
   name = "nauty-${version}";
-  version = "26r10";
+  version = "26r11";
   src = fetchurl {
     url = "http://pallini.di.uniroma1.it/nauty${version}.tar.gz";
-    sha256 = "16pdklh066z6mx424wkisr88fz9divn2caj7ggs03wy3y848spq6";
+    sha256 = "05z6mk7c31j70md83396cdjmvzzip1hqb88pfszzc6k4gy8h3m2y";
   };
   buildInputs = [];
   installPhase = ''
diff --git a/pkgs/applications/science/math/pynac/default.nix b/pkgs/applications/science/math/pynac/default.nix
index 1a059aeb1670..9bbb695a331b 100644
--- a/pkgs/applications/science/math/pynac/default.nix
+++ b/pkgs/applications/science/math/pynac/default.nix
@@ -41,6 +41,7 @@ stdenv.mkDerivation rec {
       of the full GiNaC, and it is *only* meant to be used as a Python library.
     '';
     homepage    = http://pynac.org;
+    license = licenses.gpl3;
     maintainers = with maintainers; [ timokau ];
     platforms   = platforms.linux;
   };
diff --git a/pkgs/applications/science/math/ripser/default.nix b/pkgs/applications/science/math/ripser/default.nix
index 21948a279d07..5e0b7fc300ba 100644
--- a/pkgs/applications/science/math/ripser/default.nix
+++ b/pkgs/applications/science/math/ripser/default.nix
@@ -8,7 +8,8 @@
 
 with stdenv.lib;
 
-assert elem fileFormat ["lowerTriangularCsv" "upperTriangularCsv" "dipha"];
+assert assertOneOf "fileFormat" fileFormat
+  ["lowerTriangularCsv" "upperTriangularCsv" "dipha"];
 assert useGoogleHashmap -> sparsehash != null;
 
 let
diff --git a/pkgs/applications/science/math/sage/default.nix b/pkgs/applications/science/math/sage/default.nix
index 08e3a752b8b6..7e62f0cf75ee 100644
--- a/pkgs/applications/science/math/sage/default.nix
+++ b/pkgs/applications/science/math/sage/default.nix
@@ -21,7 +21,7 @@ let
 
       sagelib = self.callPackage ./sagelib.nix {
         inherit flint ecl arb;
-        inherit sage-src pynac singular;
+        inherit sage-src openblas-blas-pc openblas-cblas-pc openblas-lapack-pc pynac singular;
         linbox = nixpkgs.linbox.override { withSage = true; };
       };
 
@@ -41,13 +41,13 @@ let
       };
 
       sage-env = self.callPackage ./sage-env.nix {
-        inherit sage-src python rWrapper ecl singular palp flint pynac pythonEnv;
+        inherit sage-src python rWrapper openblas-cblas-pc ecl singular palp flint pynac pythonEnv;
         pkg-config = nixpkgs.pkgconfig; # not to confuse with pythonPackages.pkgconfig
       };
 
       sage-with-env = self.callPackage ./sage-with-env.nix {
         inherit pythonEnv;
-        inherit sage-src pynac singular;
+        inherit sage-src openblas-blas-pc openblas-cblas-pc openblas-lapack-pc pynac singular;
         pkg-config = nixpkgs.pkgconfig; # not to confuse with pythonPackages.pkgconfig
         three = nodePackages_8_x.three;
       };
@@ -60,6 +60,10 @@ let
     };
   };
 
+  openblas-blas-pc = callPackage ./openblas-pc.nix { name = "blas"; };
+  openblas-cblas-pc = callPackage ./openblas-pc.nix { name = "cblas"; };
+  openblas-lapack-pc = callPackage ./openblas-pc.nix { name = "lapack"; };
+
   sage-src = callPackage ./sage-src.nix {};
 
   pythonRuntimeDeps = with python.pkgs; [
diff --git a/pkgs/applications/science/math/sage/env-locations.nix b/pkgs/applications/science/math/sage/env-locations.nix
index 288ffd6e0e1a..098ce3925cf3 100644
--- a/pkgs/applications/science/math/sage/env-locations.nix
+++ b/pkgs/applications/science/math/sage/env-locations.nix
@@ -38,6 +38,7 @@ writeTextFile rec {
     export COMBINATORIAL_DESIGN_DATA_DIR="${combinatorial_designs}/share/combinatorial_designs"
     export CREMONA_MINI_DATA_DIR="${elliptic_curves}/share/cremona"
     export JMOL_DIR="${jmol}"
+    export JSMOL_DIR="${jmol}/share/jsmol"
     export MATHJAX_DIR="${mathjax}/lib/node_modules/mathjax"
     export THREEJS_DIR="${three}/lib/node_modules/three"
     export SAGE_INCLUDE_DIRECTORIES="${cysignals}/lib/python2.7/site-packages"
diff --git a/pkgs/applications/science/math/sage/openblas-pc.nix b/pkgs/applications/science/math/sage/openblas-pc.nix
new file mode 100644
index 000000000000..f4669a6557e9
--- /dev/null
+++ b/pkgs/applications/science/math/sage/openblas-pc.nix
@@ -0,0 +1,17 @@
+{ openblasCompat
+, writeTextFile
+, name
+}:
+
+writeTextFile {
+  name = "openblas-${name}-pc-${openblasCompat.version}";
+  destination = "/lib/pkgconfig/${name}.pc";
+  text = ''
+    Name: ${name}
+    Version: ${openblasCompat.version}
+
+    Description: ${name} for SageMath, provided by the OpenBLAS package.
+    Cflags: -I${openblasCompat}/include
+    Libs: -L${openblasCompat}/lib -lopenblas
+  '';
+}
diff --git a/pkgs/applications/science/math/sage/patches/Only-test-py2-py3-optional-tests-when-all-of-sage-is.patch b/pkgs/applications/science/math/sage/patches/Only-test-py2-py3-optional-tests-when-all-of-sage-is.patch
new file mode 100644
index 000000000000..8cd80281d0e4
--- /dev/null
+++ b/pkgs/applications/science/math/sage/patches/Only-test-py2-py3-optional-tests-when-all-of-sage-is.patch
@@ -0,0 +1,35 @@
+From 8218bd4fdeb4c92de8af0d3aabec55980fc4fb3d Mon Sep 17 00:00:00 2001
+From: Timo Kaufmann <timokau@zoho.com>
+Date: Sun, 21 Oct 2018 17:52:40 +0200
+Subject: [PATCH] Only test py2/py3 optional tests when all of sage is tested
+
+---
+ src/sage/doctest/control.py | 5 +++--
+ 1 file changed, 3 insertions(+), 2 deletions(-)
+
+diff --git a/src/sage/doctest/control.py b/src/sage/doctest/control.py
+index bf18df8b2b..935c67abf7 100644
+--- a/src/sage/doctest/control.py
++++ b/src/sage/doctest/control.py
+@@ -362,7 +362,8 @@ class DocTestController(SageObject):
+                     if not optionaltag_regex.search(o):
+                         raise ValueError('invalid optional tag {!r}'.format(o))
+ 
+-                options.optional |= auto_optional_tags
++                if "sage" in options.optional:
++                    options.optional |= auto_optional_tags
+ 
+         self.options = options
+ 
+@@ -765,7 +766,7 @@ class DocTestController(SageObject):
+             sage: DC = DocTestController(DD, [dirname])
+             sage: DC.expand_files_into_sources()
+             sage: sorted(DC.sources[0].options.optional)  # abs tol 1
+-            ['guava', 'magma', 'py2']
++            ['guava', 'magma']
+ 
+         We check that files are skipped appropriately::
+ 
+-- 
+2.18.1
+
diff --git a/pkgs/applications/science/math/sage/patches/dochtml-optional.patch b/pkgs/applications/science/math/sage/patches/dochtml-optional.patch
deleted file mode 100644
index a51e30312ed9..000000000000
--- a/pkgs/applications/science/math/sage/patches/dochtml-optional.patch
+++ /dev/null
@@ -1,127 +0,0 @@
-diff --git a/src/doc/common/conf.py b/src/doc/common/conf.py
-index 25f94f7b7d..9f6139ea4a 100644
---- a/src/doc/common/conf.py
-+++ b/src/doc/common/conf.py
-@@ -622,9 +622,9 @@ def call_intersphinx(app, env, node, contnode):
-     Check that the link from the thematic tutorials to the reference
-     manual is relative, see :trac:`20118`::
- 
--        sage: from sage.env import SAGE_DOC
--        sage: thematic_index = os.path.join(SAGE_DOC, "html", "en", "thematic_tutorials", "index.html")
--        sage: for line in open(thematic_index).readlines():
-+        sage: from sage.env import SAGE_DOC  # optional - dochtml
-+        sage: thematic_index = os.path.join(SAGE_DOC, "html", "en", "thematic_tutorials", "index.html")  # optional - dochtml
-+        sage: for line in open(thematic_index).readlines():  # optional - dochtml
-         ....:     if "padics" in line:
-         ....:         sys.stdout.write(line)
-         <li><a class="reference external" href="../reference/padics/sage/rings/padics/tutorial.html#sage-rings-padics-tutorial" title="(in Sage Reference Manual: p-Adics ...)"><span>Introduction to the -adics</span></a></li>
-diff --git a/src/sage/doctest/control.py b/src/sage/doctest/control.py
-index 4236fd05e0..8e499cbaf7 100644
---- a/src/sage/doctest/control.py
-+++ b/src/sage/doctest/control.py
-@@ -87,7 +87,7 @@ class DocTestDefaults(SageObject):
-         self.sagenb = False
-         self.long = False
-         self.warn_long = None
--        self.optional = set(['sage']) | auto_optional_tags
-+        self.optional = set(['sage', 'dochtml']) | auto_optional_tags
-         self.randorder = None
-         self.global_iterations = 1  # sage-runtests default is 0
-         self.file_iterations = 1    # sage-runtests default is 0
-@@ -343,7 +343,8 @@ class DocTestController(SageObject):
-                     if not optionaltag_regex.search(o):
-                         raise ValueError('invalid optional tag {!r}'.format(o))
- 
--                options.optional |= auto_optional_tags
-+                if "sage" in options.optional:
-+                    options.optional |= auto_optional_tags
- 
-         self.options = options
-         self.files = args
-@@ -741,7 +742,7 @@ class DocTestController(SageObject):
-             sage: DC = DocTestController(DD, [dirname])
-             sage: DC.expand_files_into_sources()
-             sage: sorted(DC.sources[0].options.optional)  # abs tol 1
--            ['guava', 'magma', 'py3']
-+            ['guava', 'magma']
- 
-         We check that files are skipped appropriately::
- 
-@@ -968,7 +969,7 @@ class DocTestController(SageObject):
-             sage: from sage.doctest.control import DocTestDefaults, DocTestController
-             sage: DC = DocTestController(DocTestDefaults(), [])
-             sage: DC._optional_tags_string()
--            'sage'
-+            'dochtml,sage'
-             sage: DC = DocTestController(DocTestDefaults(optional="all,and,some,more"), [])
-             sage: DC._optional_tags_string()
-             'all'
-diff --git a/src/sage/misc/sagedoc.py b/src/sage/misc/sagedoc.py
-index 9255aa848f..cc4712d3ec 100644
---- a/src/sage/misc/sagedoc.py
-+++ b/src/sage/misc/sagedoc.py
-@@ -18,9 +18,9 @@ TESTS:
- Check that argspecs of extension function/methods appear correctly,
- see :trac:`12849`::
- 
--    sage: from sage.env import SAGE_DOC
--    sage: docfilename = os.path.join(SAGE_DOC, 'html', 'en', 'reference', 'calculus', 'sage', 'symbolic', 'expression.html')
--    sage: with open(docfilename) as fobj:
-+    sage: from sage.env import SAGE_DOC  # optional - dochtml
-+    sage: docfilename = os.path.join(SAGE_DOC, 'html', 'en', 'reference', 'calculus', 'sage', 'symbolic', 'expression.html')  # optional - dochtml
-+    sage: with open(docfilename) as fobj:  # optional - dochtml
-     ....:     for line in fobj:
-     ....:         if "#sage.symbolic.expression.Expression.numerical_approx" in line:
-     ....:             print(line)
-@@ -790,11 +790,12 @@ def _search_src_or_doc(what, string, extra1='', extra2='', extra3='',
- 
-     ::
- 
--        sage: len(_search_src_or_doc('src', r'matrix\(', 'incidence_structures', 'self', 'combinat', interact=False).splitlines()) > 1
-+        sage: from sage.misc.sagedoc import _search_src_or_doc  # optional - dochtml
-+        sage: len(_search_src_or_doc('src', r'matrix\(', 'incidence_structures', 'self', 'combinat', interact=False).splitlines()) > 1  # optional - dochtml
-         True
--        sage: 'abvar/homology' in _search_src_or_doc('doc', 'homology', 'variety', interact=False)  # long time (4s on sage.math, 2012)
-+        sage: 'abvar/homology' in _search_src_or_doc('doc', 'homology', 'variety', interact=False)  # optional - dochtml, long time (4s on sage.math, 2012)
-         True
--        sage: 'divisors' in _search_src_or_doc('src', '^ *def prime', interact=False)
-+        sage: 'divisors' in _search_src_or_doc('src', '^ *def prime', interact=False)  # optional - dochtml
-         True
-     """
-     # process keywords
-@@ -1160,9 +1161,9 @@ def search_doc(string, extra1='', extra2='', extra3='', extra4='',
-     counting the length of ``search_doc('tree',
-     interact=False).splitlines()`` gives the number of matches. ::
- 
--        sage: len(search_doc('tree', interact=False).splitlines()) > 4000  # long time
-+        sage: len(search_doc('tree', interact=False).splitlines()) > 4000  # optional - dochtml, long time
-         True
--        sage: len(search_doc('tree', whole_word=True, interact=False).splitlines()) < 2000  # long time
-+        sage: len(search_doc('tree', whole_word=True, interact=False).splitlines()) < 2000  # optional - dochtml, long time
-         True
-     """
-     return _search_src_or_doc('doc', string, extra1=extra1, extra2=extra2,
-@@ -1332,9 +1333,9 @@ class _sage_doc:
- 
-     EXAMPLES::
- 
--        sage: browse_sage_doc._open("reference", testing=True)[0]  # indirect doctest
-+        sage: browse_sage_doc._open("reference", testing=True)[0]  # optional - dochtml, indirect doctest
-         'http://localhost:8000/doc/live/reference/index.html'
--        sage: browse_sage_doc(identity_matrix, 'rst')[-107:-47]
-+        sage: browse_sage_doc(identity_matrix, 'rst')[-107:-47]  # optional - dochtml
-         'Full MatrixSpace of 3 by 3 sparse matrices over Integer Ring'
-     """
-     def __init__(self):
-@@ -1494,9 +1495,9 @@ class _sage_doc:
- 
-         EXAMPLES::
- 
--            sage: browse_sage_doc._open("reference", testing=True)[0]
-+            sage: browse_sage_doc._open("reference", testing=True)[0]  # optional - dochtml
-             'http://localhost:8000/doc/live/reference/index.html'
--            sage: browse_sage_doc._open("tutorial", testing=True)[1]
-+            sage: browse_sage_doc._open("tutorial", testing=True)[1]  # optional - dochtml
-             '.../html/en/tutorial/index.html'
-         """
-         url = self._base_url + os.path.join(name, "index.html")
diff --git a/pkgs/applications/science/math/sage/patches/eclib-20180710.patch b/pkgs/applications/science/math/sage/patches/eclib-20180710.patch
index d06e1e6cedf2..986ae42aeb62 100644
--- a/pkgs/applications/science/math/sage/patches/eclib-20180710.patch
+++ b/pkgs/applications/science/math/sage/patches/eclib-20180710.patch
@@ -14,27 +14,3 @@ index 4417b59276..ae57ca2991 100644
      """
      global instances
      try:
-diff --git a/src/sage/libs/eclib/wrap.cpp b/src/sage/libs/eclib/wrap.cpp
-index 5fd5693b53..d12468faa8 100644
---- a/src/sage/libs/eclib/wrap.cpp
-+++ b/src/sage/libs/eclib/wrap.cpp
-@@ -133,8 +133,8 @@ char* Curvedata_isogeny_class(struct Curvedata* E, int verbose)
- 
- 
- int mw_process(struct Curvedata* curve, struct mw* m,
--                      const struct bigint* x, const struct bigint* y,
--                      const struct bigint* z, int sat)
-+                      const bigint* x, const bigint* y,
-+                      const bigint* z, int sat)
- {
-   Point P(*curve, *x, *y, *z);
-   if (!P.isvalid())
-@@ -188,7 +188,7 @@ int mw_rank(struct mw* m)
- }
- 
- /* Returns index and unsat long array, which user must deallocate */
--int mw_saturate(struct mw* m, struct bigint* index, char** unsat,
-+int mw_saturate(struct mw* m, bigint* index, char** unsat,
-                        long sat_bd, int odd_primes_only)
- {
-   vector<long> v;
diff --git a/pkgs/applications/science/math/sage/patches/numpy-1.14.3.patch b/pkgs/applications/science/math/sage/patches/numpy-1.15.1.patch
index 5927bc116096..9e855ba4ad94 100644
--- a/pkgs/applications/science/math/sage/patches/numpy-1.14.3.patch
+++ b/pkgs/applications/science/math/sage/patches/numpy-1.15.1.patch
@@ -1,5 +1,5 @@
 diff --git a/src/doc/en/faq/faq-usage.rst b/src/doc/en/faq/faq-usage.rst
-index 79b4205fd3..9a89bd2136 100644
+index 2347a1190d..f5b0fe71a4 100644
 --- a/src/doc/en/faq/faq-usage.rst
 +++ b/src/doc/en/faq/faq-usage.rst
 @@ -338,7 +338,7 @@ ints. For example::
@@ -174,7 +174,7 @@ index 5b89cd75ee..e50b2ea5d4 100644
  This creates a random 5x5 matrix ``A``, and solves `Ax=b` where
  ``b=[0.0,1.0,2.0,3.0,4.0]``. There are many other routines in the :mod:`numpy.linalg`
 diff --git a/src/sage/calculus/riemann.pyx b/src/sage/calculus/riemann.pyx
-index df85cce43d..34ea164be0 100644
+index 60f37f7557..4ac3dedf1d 100644
 --- a/src/sage/calculus/riemann.pyx
 +++ b/src/sage/calculus/riemann.pyx
 @@ -1191,30 +1191,30 @@ cpdef complex_to_spiderweb(np.ndarray[COMPLEX_T, ndim = 2] z_values,
@@ -248,7 +248,7 @@ index df85cce43d..34ea164be0 100644
  
      TESTS::
 diff --git a/src/sage/combinat/fully_packed_loop.py b/src/sage/combinat/fully_packed_loop.py
-index 61b1003002..4baee9cbbd 100644
+index 0a9bd61267..d2193cc2d6 100644
 --- a/src/sage/combinat/fully_packed_loop.py
 +++ b/src/sage/combinat/fully_packed_loop.py
 @@ -72,11 +72,11 @@ def _make_color_list(n, colors=None,  color_map=None, randomize=False):
@@ -269,10 +269,10 @@ index 61b1003002..4baee9cbbd 100644
          ['blue', 'blue', 'red', 'blue', 'red', 'red', 'red', 'blue']
      """
 diff --git a/src/sage/finance/time_series.pyx b/src/sage/finance/time_series.pyx
-index c37700d14e..49b7298d0b 100644
+index 28779365df..3ab0282861 100644
 --- a/src/sage/finance/time_series.pyx
 +++ b/src/sage/finance/time_series.pyx
-@@ -109,8 +109,8 @@ cdef class TimeSeries:
+@@ -111,8 +111,8 @@ cdef class TimeSeries:
  
              sage: import numpy
              sage: v = numpy.array([[1,2], [3,4]], dtype=float); v
@@ -283,7 +283,7 @@ index c37700d14e..49b7298d0b 100644
              sage: finance.TimeSeries(v)
              [1.0000, 2.0000, 3.0000, 4.0000]
              sage: finance.TimeSeries(v[:,0])
-@@ -2098,14 +2098,14 @@ cdef class TimeSeries:
+@@ -2100,14 +2100,14 @@ cdef class TimeSeries:
  
              sage: w[0] = 20
              sage: w
@@ -301,7 +301,7 @@ index c37700d14e..49b7298d0b 100644
              sage: v
              [20.0000, -3.0000, 4.5000, -2.0000]
 diff --git a/src/sage/functions/hyperbolic.py b/src/sage/functions/hyperbolic.py
-index 931a4b41e4..bf33fc483d 100644
+index aff552f450..7a6df931e7 100644
 --- a/src/sage/functions/hyperbolic.py
 +++ b/src/sage/functions/hyperbolic.py
 @@ -214,7 +214,7 @@ class Function_coth(GinacFunction):
@@ -341,7 +341,7 @@ index 931a4b41e4..bf33fc483d 100644
          return arctanh(1.0 / x)
  
 diff --git a/src/sage/functions/orthogonal_polys.py b/src/sage/functions/orthogonal_polys.py
-index 017c85a96f..33fbb499c5 100644
+index ed6365bef4..99b8b04dad 100644
 --- a/src/sage/functions/orthogonal_polys.py
 +++ b/src/sage/functions/orthogonal_polys.py
 @@ -810,12 +810,12 @@ class Func_chebyshev_T(ChebyshevFunction):
@@ -379,10 +379,10 @@ index 017c85a96f..33fbb499c5 100644
              array([ 0.2 , -0.96])
          """
 diff --git a/src/sage/functions/other.py b/src/sage/functions/other.py
-index 679384c907..d63b295a4c 100644
+index 1883daa3e6..9885222817 100644
 --- a/src/sage/functions/other.py
 +++ b/src/sage/functions/other.py
-@@ -390,7 +390,7 @@ class Function_ceil(BuiltinFunction):
+@@ -389,7 +389,7 @@ class Function_ceil(BuiltinFunction):
              sage: import numpy
              sage: a = numpy.linspace(0,2,6)
              sage: ceil(a)
@@ -391,7 +391,7 @@ index 679384c907..d63b295a4c 100644
  
          Test pickling::
  
-@@ -539,7 +539,7 @@ class Function_floor(BuiltinFunction):
+@@ -553,7 +553,7 @@ class Function_floor(BuiltinFunction):
              sage: import numpy
              sage: a = numpy.linspace(0,2,6)
              sage: floor(a)
@@ -400,7 +400,7 @@ index 679384c907..d63b295a4c 100644
              sage: floor(x)._sympy_()
              floor(x)
  
-@@ -840,7 +840,7 @@ def sqrt(x, *args, **kwds):
+@@ -869,7 +869,7 @@ def sqrt(x, *args, **kwds):
              sage: import numpy
              sage: a = numpy.arange(2,5)
              sage: sqrt(a)
@@ -409,11 +409,35 @@ index 679384c907..d63b295a4c 100644
          """
          if isinstance(x, float):
              return math.sqrt(x)
+diff --git a/src/sage/functions/spike_function.py b/src/sage/functions/spike_function.py
+index 1e021de3fe..56635ca98f 100644
+--- a/src/sage/functions/spike_function.py
++++ b/src/sage/functions/spike_function.py
+@@ -157,7 +157,7 @@ class SpikeFunction:
+             sage: S = spike_function([(-3,4),(-1,1),(2,3)]); S
+             A spike function with spikes at [-3.0, -1.0, 2.0]
+             sage: P = S.plot_fft_abs(8)
+-            sage: p = P[0]; p.ydata
++            sage: p = P[0]; p.ydata  # abs tol 1e-8
+             [5.0, 5.0, 3.367958691924177, 3.367958691924177, 4.123105625617661, 4.123105625617661, 4.759921664218055, 4.759921664218055]
+         """
+         w = self.vector(samples = samples, xmin=xmin, xmax=xmax)
+@@ -176,8 +176,8 @@ class SpikeFunction:
+             sage: S = spike_function([(-3,4),(-1,1),(2,3)]); S
+             A spike function with spikes at [-3.0, -1.0, 2.0]
+             sage: P = S.plot_fft_arg(8)
+-            sage: p = P[0]; p.ydata
+-            [0.0, 0.0, -0.211524990023434..., -0.211524990023434..., 0.244978663126864..., 0.244978663126864..., -0.149106180027477..., -0.149106180027477...]
++            sage: p = P[0]; p.ydata  # abs tol 1e-8
++            [0.0, 0.0, -0.211524990023434, -0.211524990023434, 0.244978663126864, 0.244978663126864, -0.149106180027477, -0.149106180027477]
+         """
+         w = self.vector(samples = samples, xmin=xmin, xmax=xmax)
+         xmin, xmax = self._ranges(xmin, xmax)
 diff --git a/src/sage/functions/trig.py b/src/sage/functions/trig.py
-index e7e7a311cd..e7ff78a9de 100644
+index 501e7ff6b6..5f760912f0 100644
 --- a/src/sage/functions/trig.py
 +++ b/src/sage/functions/trig.py
-@@ -731,7 +731,7 @@ class Function_arccot(GinacFunction):
+@@ -724,7 +724,7 @@ class Function_arccot(GinacFunction):
              sage: import numpy
              sage: a = numpy.arange(2, 5)
              sage: arccot(a)
@@ -422,7 +446,7 @@ index e7e7a311cd..e7ff78a9de 100644
          """
          return math.pi/2 - arctan(x)
  
-@@ -787,7 +787,7 @@ class Function_arccsc(GinacFunction):
+@@ -780,7 +780,7 @@ class Function_arccsc(GinacFunction):
              sage: import numpy
              sage: a = numpy.arange(2, 5)
              sage: arccsc(a)
@@ -431,7 +455,7 @@ index e7e7a311cd..e7ff78a9de 100644
          """
          return arcsin(1.0/x)
  
-@@ -845,7 +845,7 @@ class Function_arcsec(GinacFunction):
+@@ -838,7 +838,7 @@ class Function_arcsec(GinacFunction):
              sage: import numpy
              sage: a = numpy.arange(2, 5)
              sage: arcsec(a)
@@ -440,7 +464,7 @@ index e7e7a311cd..e7ff78a9de 100644
          """
          return arccos(1.0/x)
  
-@@ -920,13 +920,13 @@ class Function_arctan2(GinacFunction):
+@@ -913,13 +913,13 @@ class Function_arctan2(GinacFunction):
              sage: a = numpy.linspace(1, 3, 3)
              sage: b = numpy.linspace(3, 6, 3)
              sage: atan2(a, b)
@@ -458,10 +482,10 @@ index e7e7a311cd..e7ff78a9de 100644
          TESTS::
  
 diff --git a/src/sage/matrix/constructor.pyx b/src/sage/matrix/constructor.pyx
-index 19a1d37df0..5780dfae1c 100644
+index 12136f1773..491bf22e62 100644
 --- a/src/sage/matrix/constructor.pyx
 +++ b/src/sage/matrix/constructor.pyx
-@@ -494,8 +494,8 @@ class MatrixFactory(object):
+@@ -503,8 +503,8 @@ def matrix(*args, **kwds):
          [7 8 9]
          Full MatrixSpace of 3 by 3 dense matrices over Integer Ring
          sage: n = matrix(QQ, 2, 2, [1, 1/2, 1/3, 1/4]).numpy(); n
@@ -473,10 +497,31 @@ index 19a1d37df0..5780dfae1c 100644
          [  1 1/2]
          [1/3 1/4]
 diff --git a/src/sage/matrix/matrix_double_dense.pyx b/src/sage/matrix/matrix_double_dense.pyx
-index 48e0a8a97f..1be5d35b19 100644
+index 66e54a79a4..0498334f4b 100644
 --- a/src/sage/matrix/matrix_double_dense.pyx
 +++ b/src/sage/matrix/matrix_double_dense.pyx
-@@ -2546,7 +2546,7 @@ cdef class Matrix_double_dense(Matrix_dense):
+@@ -606,6 +606,9 @@ cdef class Matrix_double_dense(Matrix_dense):
+             [ 3.0 + 9.0*I 4.0 + 16.0*I 5.0 + 25.0*I]
+             [6.0 + 36.0*I 7.0 + 49.0*I 8.0 + 64.0*I]
+             sage: B.condition()
++            doctest:warning
++            ...
++            ComplexWarning: Casting complex values to real discards the imaginary part
+             203.851798...
+             sage: B.condition(p='frob')
+             203.851798...
+@@ -654,9 +657,7 @@ cdef class Matrix_double_dense(Matrix_dense):
+             True
+             sage: B = A.change_ring(CDF)
+             sage: B.condition()
+-            Traceback (most recent call last):
+-            ...
+-            LinAlgError: Singular matrix
++            +Infinity
+ 
+         Improper values of ``p`` are caught.  ::
+ 
+@@ -2519,7 +2520,7 @@ cdef class Matrix_double_dense(Matrix_dense):
              sage: P.is_unitary(algorithm='orthonormal')
              Traceback (most recent call last):
              ...
@@ -485,7 +530,7 @@ index 48e0a8a97f..1be5d35b19 100644
  
          TESTS::
  
-@@ -3662,8 +3662,8 @@ cdef class Matrix_double_dense(Matrix_dense):
+@@ -3635,8 +3636,8 @@ cdef class Matrix_double_dense(Matrix_dense):
              [0.0 1.0 2.0]
              [3.0 4.0 5.0]
              sage: m.numpy()
@@ -496,7 +541,7 @@ index 48e0a8a97f..1be5d35b19 100644
  
          Alternatively, numpy automatically calls this function (via
          the magic :meth:`__array__` method) to convert Sage matrices
-@@ -3674,16 +3674,16 @@ cdef class Matrix_double_dense(Matrix_dense):
+@@ -3647,16 +3648,16 @@ cdef class Matrix_double_dense(Matrix_dense):
              [0.0 1.0 2.0]
              [3.0 4.0 5.0]
              sage: numpy.array(m)
@@ -518,10 +563,10 @@ index 48e0a8a97f..1be5d35b19 100644
              dtype('complex128')
  
 diff --git a/src/sage/matrix/special.py b/src/sage/matrix/special.py
-index c698ba5e97..b743bab354 100644
+index ccbd208810..c3f9a65093 100644
 --- a/src/sage/matrix/special.py
 +++ b/src/sage/matrix/special.py
-@@ -705,7 +705,7 @@ def diagonal_matrix(arg0=None, arg1=None, arg2=None, sparse=True):
+@@ -706,7 +706,7 @@ def diagonal_matrix(arg0=None, arg1=None, arg2=None, sparse=True):
  
          sage: import numpy
          sage: entries = numpy.array([1.2, 5.6]); entries
@@ -530,7 +575,7 @@ index c698ba5e97..b743bab354 100644
          sage: A = diagonal_matrix(3, entries); A
          [1.2 0.0 0.0]
          [0.0 5.6 0.0]
-@@ -715,7 +715,7 @@ def diagonal_matrix(arg0=None, arg1=None, arg2=None, sparse=True):
+@@ -716,7 +716,7 @@ def diagonal_matrix(arg0=None, arg1=None, arg2=None, sparse=True):
  
          sage: j = numpy.complex(0,1)
          sage: entries = numpy.array([2.0+j, 8.1, 3.4+2.6*j]); entries
@@ -540,10 +585,10 @@ index c698ba5e97..b743bab354 100644
          [2.0 + 1.0*I         0.0         0.0]
          [        0.0         8.1         0.0]
 diff --git a/src/sage/modules/free_module_element.pyx b/src/sage/modules/free_module_element.pyx
-index 230f142117..2ab1c0ae68 100644
+index 37d92c1282..955d083b34 100644
 --- a/src/sage/modules/free_module_element.pyx
 +++ b/src/sage/modules/free_module_element.pyx
-@@ -982,7 +982,7 @@ cdef class FreeModuleElement(Vector):   # abstract base class
+@@ -988,7 +988,7 @@ cdef class FreeModuleElement(Vector):   # abstract base class
              sage: v.numpy()
              array([1, 2, 5/6], dtype=object)
              sage: v.numpy(dtype=float)
@@ -552,7 +597,7 @@ index 230f142117..2ab1c0ae68 100644
              sage: v.numpy(dtype=int)
              array([1, 2, 0])
              sage: import numpy
-@@ -993,7 +993,7 @@ cdef class FreeModuleElement(Vector):   # abstract base class
+@@ -999,7 +999,7 @@ cdef class FreeModuleElement(Vector):   # abstract base class
          be more efficient but may have unintended consequences::
  
              sage: v.numpy(dtype=None)
@@ -596,22 +641,6 @@ index 39fc2970de..2badf98284 100644
          """
          if dtype is None or dtype is self._vector_numpy.dtype:
              from copy import copy
-diff --git a/src/sage/numerical/optimize.py b/src/sage/numerical/optimize.py
-index 17b5ebb84b..92ce35c502 100644
---- a/src/sage/numerical/optimize.py
-+++ b/src/sage/numerical/optimize.py
-@@ -486,9 +486,9 @@ def minimize_constrained(func,cons,x0,gradient=None,algorithm='default', **args)
-                 else:
-                     min = optimize.fmin_tnc(f, x0, approx_grad=True, bounds=cons, messages=0, **args)[0]
-         elif isinstance(cons[0], function_type) or isinstance(cons[0], Expression):
--            min = optimize.fmin_cobyla(f, x0, cons, iprint=0, **args)
-+            min = optimize.fmin_cobyla(f, x0, cons, disp=0, **args)
-     elif isinstance(cons, function_type) or isinstance(cons, Expression):
--        min = optimize.fmin_cobyla(f, x0, cons, iprint=0, **args)
-+        min = optimize.fmin_cobyla(f, x0, cons, disp=0, **args)
-     return vector(RDF, min)
- 
- 
 diff --git a/src/sage/plot/complex_plot.pyx b/src/sage/plot/complex_plot.pyx
 index ad9693da62..758fb709b7 100644
 --- a/src/sage/plot/complex_plot.pyx
@@ -649,6 +678,76 @@ index ad9693da62..758fb709b7 100644
      """
      import numpy
      cdef unsigned int i, j, imax, jmax
+diff --git a/src/sage/plot/histogram.py b/src/sage/plot/histogram.py
+index 5d28473731..fc4b2046c0 100644
+--- a/src/sage/plot/histogram.py
++++ b/src/sage/plot/histogram.py
+@@ -53,10 +53,17 @@ class Histogram(GraphicPrimitive):
+         """
+         import numpy as np
+         self.datalist=np.asarray(datalist,dtype=float)
++        if 'normed' in options:
++            from sage.misc.superseded import deprecation
++            deprecation(25260, "the 'normed' option is deprecated. Use 'density' instead.")
+         if 'linestyle' in options:
+             from sage.plot.misc import get_matplotlib_linestyle
+             options['linestyle'] = get_matplotlib_linestyle(
+                     options['linestyle'], return_type='long')
++        if options.get('range', None):
++            # numpy.histogram performs type checks on "range" so this must be
++            # actual floats
++            options['range'] = [float(x) for x in options['range']]
+         GraphicPrimitive.__init__(self, options)
+ 
+     def get_minmax_data(self):
+@@ -80,10 +87,14 @@ class Histogram(GraphicPrimitive):
+             {'xmax': 4.0, 'xmin': 0, 'ymax': 2, 'ymin': 0}
+ 
+         TESTS::
+-
+             sage: h = histogram([10,3,5], normed=True)[0]
+-            sage: h.get_minmax_data()  # rel tol 1e-15
+-            {'xmax': 10.0, 'xmin': 3.0, 'ymax': 0.4761904761904765, 'ymin': 0}
++            doctest:warning...:
++            DeprecationWarning: the 'normed' option is deprecated. Use 'density' instead.
++            See https://trac.sagemath.org/25260 for details.
++            sage: h.get_minmax_data()
++            doctest:warning ...:
++            VisibleDeprecationWarning: Passing `normed=True` on non-uniform bins has always been broken, and computes neither the probability density function nor the probability mass function. The result is only correct if the bins are uniform, when density=True will produce the same result anyway. The argument will be removed in a future version of numpy.
++            {'xmax': 10.0, 'xmin': 3.0, 'ymax': 0.476190476190..., 'ymin': 0}
+         """
+         import numpy
+ 
+@@ -152,7 +163,7 @@ class Histogram(GraphicPrimitive):
+                 'rwidth': 'The relative width of the bars as a fraction of the bin width',
+                 'cumulative': '(True or False) If True, then a histogram is computed in which each bin gives the counts in that bin plus all bins for smaller values.  Negative values give a reversed direction of accumulation.',
+                 'range': 'A list [min, max] which define the range of the histogram. Values outside of this range are treated as outliers and omitted from counts.',
+-                'normed': 'Deprecated alias for density',
++                'normed': 'Deprecated. Use density instead.',
+                 'density': '(True or False) If True, the counts are normalized to form a probability density. (n/(len(x)*dbin)',
+                 'weights': 'A sequence of weights the same length as the data list. If supplied, then each value contributes its associated weight to the bin count.',
+                 'stacked': '(True or False) If True, multiple data are stacked on top of each other.',
+@@ -199,7 +210,7 @@ class Histogram(GraphicPrimitive):
+             subplot.hist(self.datalist.transpose(), **options)
+ 
+ 
+-@options(aspect_ratio='automatic',align='mid', weights=None, range=None, bins=10, edgecolor='black')
++@options(aspect_ratio='automatic', align='mid', weights=None, range=None, bins=10, edgecolor='black')
+ def histogram(datalist, **options):
+     """
+     Computes and draws the histogram for list(s) of numerical data.
+@@ -231,8 +242,9 @@ def histogram(datalist, **options):
+     - ``linewidth`` -- (float) width of the lines defining the bars
+     - ``linestyle`` -- (default: 'solid') Style of the line. One of 'solid'
+       or '-', 'dashed' or '--', 'dotted' or ':', 'dashdot' or '-.'
+-    - ``density`` -- (boolean - default: False) If True, the counts are
+-      normalized to form a probability density.
++    - ``density`` -- (boolean - default: False) If True, the result is the
++      value of the probability density function at the bin, normalized such
++      that the integral over the range is 1.
+     - ``range`` -- A list [min, max] which define the range of the
+       histogram. Values outside of this range are treated as outliers and
+       omitted from counts
 diff --git a/src/sage/plot/line.py b/src/sage/plot/line.py
 index 23f5e61446..3b1b51d7cf 100644
 --- a/src/sage/plot/line.py
@@ -718,7 +817,7 @@ index f3da57c370..3806f4b32f 100644
          TESTS:
  
 diff --git a/src/sage/probability/probability_distribution.pyx b/src/sage/probability/probability_distribution.pyx
-index f66cd898b9..35995886d5 100644
+index 1b119e323f..3290b00695 100644
 --- a/src/sage/probability/probability_distribution.pyx
 +++ b/src/sage/probability/probability_distribution.pyx
 @@ -130,7 +130,17 @@ cdef class ProbabilityDistribution:
@@ -741,10 +840,10 @@ index f66cd898b9..35995886d5 100644
          import pylab
          l = [float(self.get_random_element()) for _ in range(num_samples)]
 diff --git a/src/sage/rings/rational.pyx b/src/sage/rings/rational.pyx
-index a0bfe080f5..7d95e7a1a8 100644
+index 12ca1b222b..9bad7dae0c 100644
 --- a/src/sage/rings/rational.pyx
 +++ b/src/sage/rings/rational.pyx
-@@ -1056,7 +1056,7 @@ cdef class Rational(sage.structure.element.FieldElement):
+@@ -1041,7 +1041,7 @@ cdef class Rational(sage.structure.element.FieldElement):
              dtype('O')
  
              sage: numpy.array([1, 1/2, 3/4])
@@ -754,10 +853,10 @@ index a0bfe080f5..7d95e7a1a8 100644
          if mpz_cmp_ui(mpq_denref(self.value), 1) == 0:
              if mpz_fits_slong_p(mpq_numref(self.value)):
 diff --git a/src/sage/rings/real_mpfr.pyx b/src/sage/rings/real_mpfr.pyx
-index 4c630867a4..64e2187f5b 100644
+index 9b90c8833e..1ce05b937d 100644
 --- a/src/sage/rings/real_mpfr.pyx
 +++ b/src/sage/rings/real_mpfr.pyx
-@@ -1438,7 +1438,7 @@ cdef class RealNumber(sage.structure.element.RingElement):
+@@ -1439,7 +1439,7 @@ cdef class RealNumber(sage.structure.element.RingElement):
  
              sage: import numpy
              sage: numpy.arange(10.0)
@@ -767,10 +866,10 @@ index 4c630867a4..64e2187f5b 100644
              dtype('float64')
              sage: numpy.array([1.000000000000000000000000000000000000]).dtype
 diff --git a/src/sage/schemes/elliptic_curves/height.py b/src/sage/schemes/elliptic_curves/height.py
-index 3d270ebf9d..1144f168e3 100644
+index de31fe9883..7a33ea6f5b 100644
 --- a/src/sage/schemes/elliptic_curves/height.py
 +++ b/src/sage/schemes/elliptic_curves/height.py
-@@ -1623,18 +1623,18 @@ class EllipticCurveCanonicalHeight:
+@@ -1627,18 +1627,18 @@ class EllipticCurveCanonicalHeight:
          even::
  
              sage: H.wp_on_grid(v,4)
@@ -798,10 +897,10 @@ index 3d270ebf9d..1144f168e3 100644
          tau = self.tau(v)
          fk, err = self.fk_intervals(v, 15, CDF)
 diff --git a/src/sage/symbolic/ring.pyx b/src/sage/symbolic/ring.pyx
-index 2dcb0492b9..2b1a06385c 100644
+index 9da38002e8..d61e74bf82 100644
 --- a/src/sage/symbolic/ring.pyx
 +++ b/src/sage/symbolic/ring.pyx
-@@ -1135,7 +1135,7 @@ cdef class NumpyToSRMorphism(Morphism):
+@@ -1136,7 +1136,7 @@ cdef class NumpyToSRMorphism(Morphism):
          sage: cos(numpy.int('2'))
          cos(2)
          sage: numpy.cos(numpy.int('2'))
diff --git a/pkgs/applications/science/math/sage/patches/pari-no-threads.patch b/pkgs/applications/science/math/sage/patches/pari-no-threads.patch
deleted file mode 100644
index 13b47dbdd31b..000000000000
--- a/pkgs/applications/science/math/sage/patches/pari-no-threads.patch
+++ /dev/null
@@ -1,18 +0,0 @@
-diff --git a/src/sage/libs/pari/__init__.py b/src/sage/libs/pari/__init__.py
-index e451766474..77eda66097 100644
---- a/src/sage/libs/pari/__init__.py
-+++ b/src/sage/libs/pari/__init__.py
-@@ -205,6 +205,13 @@ def _get_pari_instance():
-     # messages in Sage.
-     P.default("debugmem", 0)
- 
-+    # Make sure pari doesn't use threads, regardless of how it was compiled.
-+    # Threads cause some doctest failures (memory issues). Those could probably
-+    # be solved without disabling threads. But that would require figuring out
-+    # some sensible values for `threadsizemax`. See
-+    # https://pari.math.u-bordeaux.fr/dochtml/html/GP_defaults.html
-+    P.default("nbthreads", 1)
-+
-     return P
- 
- pari = _get_pari_instance()
diff --git a/pkgs/applications/science/math/sage/patches/revert-sphinx-always-fork.patch b/pkgs/applications/science/math/sage/patches/revert-sphinx-always-fork.patch
new file mode 100644
index 000000000000..64dd6fd93777
--- /dev/null
+++ b/pkgs/applications/science/math/sage/patches/revert-sphinx-always-fork.patch
@@ -0,0 +1,71 @@
+commit f1c59929c3c180ac283334c2b3c901ac8c82f6b1
+Author: Timo Kaufmann <timokau@zoho.com>
+Date:   Sat Oct 20 20:07:41 2018 +0200
+
+    Revert "Something related to the sphinxbuild seems to be leaking memory"
+    
+    This reverts commit 7d85dc796c58c3de57401bc22d3587b94e205091.
+
+diff --git a/src/sage_setup/docbuild/__init__.py b/src/sage_setup/docbuild/__init__.py
+index 0b24b1a60b..084c3f89d7 100644
+--- a/src/sage_setup/docbuild/__init__.py
++++ b/src/sage_setup/docbuild/__init__.py
+@@ -265,29 +265,35 @@ class DocBuilder(object):
+     # import the customized builder for object.inv files
+     inventory = builder_helper('inventory')
+ 
+-def build_many(target, args):
+-    # Pool() uses an actual fork() to run each new instance. This is important
+-    # for performance reasons, i.e., don't use a forkserver when it becomes
+-    # available with Python 3: Here, sage is already initialized which is quite
+-    # costly, with a forkserver we would have to reinitialize it for every
+-    # document we build. At the same time, don't serialize this by taking the
+-    # pool (and thus the call to fork()) out completely: The call to Sphinx
+-    # leaks memory, so we need to build each document in its own process to
+-    # control the RAM usage.
+-    from multiprocessing import Pool
+-    pool = Pool(NUM_THREADS, maxtasksperchild=1)
+-    # map_async handles KeyboardInterrupt correctly. Plain map and
+-    # apply_async does not, so don't use it.
+-    x = pool.map_async(target, args, 1)
+-    try:
+-        ret = x.get(99999)
+-        pool.close()
+-        pool.join()
+-    except Exception:
+-        pool.terminate()
+-        if ABORT_ON_ERROR:
+-            raise
+-    return ret
++if NUM_THREADS > 1:
++    def build_many(target, args):
++        from multiprocessing import Pool
++        pool = Pool(NUM_THREADS, maxtasksperchild=1)
++        # map_async handles KeyboardInterrupt correctly. Plain map and
++        # apply_async does not, so don't use it.
++        x = pool.map_async(target, args, 1)
++        try:
++            ret = x.get(99999)
++            pool.close()
++            pool.join()
++        except Exception:
++            pool.terminate()
++            if ABORT_ON_ERROR:
++                raise
++        return ret
++else:
++    def build_many(target, args):
++        results = []
++
++        for arg in args:
++            try:
++                results.append(target(arg))
++            except Exception:
++                if ABORT_ON_ERROR:
++                    raise
++
++        return results
++
+ 
+ ##########################################
+ #      Parallel Building Ref Manual      #
diff --git a/pkgs/applications/science/math/sage/patches/singular-4.1.1p2.patch b/pkgs/applications/science/math/sage/patches/singular-4.1.1p2.patch
deleted file mode 100644
index 4c8df92904ed..000000000000
--- a/pkgs/applications/science/math/sage/patches/singular-4.1.1p2.patch
+++ /dev/null
@@ -1,274 +0,0 @@
-diff --git a/src/sage/interfaces/singular.py b/src/sage/interfaces/singular.py
-index 9d65c9fa6c..a028bbe719 100644
---- a/src/sage/interfaces/singular.py
-+++ b/src/sage/interfaces/singular.py
-@@ -654,7 +654,7 @@ class Singular(ExtraTabCompletion, Expect):
- 
-         s = Expect.eval(self, x, **kwds)
- 
--        if s.find("error") != -1 or s.find("Segment fault") != -1:
-+        if s.find("error occurred") != -1 or s.find("Segment fault") != -1:
-             raise SingularError('Singular error:\n%s'%s)
- 
-         if get_verbose() > 0:
-@@ -1079,7 +1079,7 @@ class Singular(ExtraTabCompletion, Expect):
-             sage: S = singular.ring('real', '(a,b)', 'lp')
-             sage: singular.current_ring()
-             polynomial ring, over a field, global ordering
--            //   coefficients: float
-+            //   coefficients: Float()
-             //   number of vars : 2
-             //        block   1 : ordering lp
-             //                  : names    a b
-@@ -1157,7 +1157,7 @@ class Singular(ExtraTabCompletion, Expect):
-              sage: singular._tab_completion()
-              ['exteriorPower',
-               ...
--              'flintZ']
-+              'crossprod']
-          """
-         p = re.compile("// *([a-z0-9A-Z_]*).*") #compiles regular expression
-         proclist = self.eval("listvar(proc)").splitlines()
-@@ -1183,7 +1183,7 @@ class Singular(ExtraTabCompletion, Expect):
-         EXAMPLES::
- 
-             sage: singular.version()
--            "Singular ... version 4.1.0 ...
-+            "Singular ... version 4...
-         """
-         return singular_version()
- 
-@@ -1562,7 +1562,7 @@ class SingularElement(ExtraTabCompletion, ExpectElement):
-         elif charstr[0] in ['0', 'QQ']:
-             from sage.all import QQ
-             br = QQ
--        elif charstr[0]=='real':
-+        elif charstr[0].startswith('Float'):
-             from sage.all import RealField, ceil, log
-             prec = singular.eval('ringlist(basering)[1][2][1]')
-             br = RealField(ceil((ZZ(prec)+1)/log(2,10)))
-@@ -1750,7 +1750,7 @@ class SingularElement(ExtraTabCompletion, ExpectElement):
- 
-         # Singular 4 puts parentheses around floats and sign outside them
-         charstr = self.parent().eval('charstr(basering)').split(',',1)
--        if charstr[0] in ['real', 'complex']:
-+        if charstr[0]=='complex' or charstr[0].startswith('Float'):
-               for i in range(coeff_start, 2 * coeff_start):
-                   singular_poly_list[i] = singular_poly_list[i].replace('(','').replace(')','')
- 
-@@ -1992,7 +1992,7 @@ class SingularElement(ExtraTabCompletion, ExpectElement):
-             sage: S = singular.ring('real', '(a,b)', 'lp')
-             sage: singular.current_ring()
-             polynomial ring, over a field, global ordering
--            //   coefficients: float
-+            //   coefficients: Float()
-             //   number of vars : 2
-             //        block   1 : ordering lp
-             //                  : names    a b
-@@ -2072,7 +2072,7 @@ class SingularElement(ExtraTabCompletion, ExpectElement):
-             sage: R._tab_completion()
-             ['exteriorPower',
-              ...
--             'flintZ']
-+             'crossprod']
-         """
-         return self.parent()._tab_completion()
- 
-@@ -2358,7 +2358,7 @@ def singular_version():
-     EXAMPLES::
- 
-         sage: singular.version()
--        "Singular ... version 4.1.0 ...
-+        "Singular ... version 4...
-     """
-     return singular.eval('system("--version");')
- 
-diff --git a/src/sage/libs/singular/decl.pxd b/src/sage/libs/singular/decl.pxd
-index 4b658c4807..d863740419 100644
---- a/src/sage/libs/singular/decl.pxd
-+++ b/src/sage/libs/singular/decl.pxd
-@@ -170,7 +170,7 @@ cdef extern from "singular/Singular/libsingular.h":
- 
-     int n_NumberOfParameters(const n_Procs_s* r)
- 
--    ctypedef struct poly "polyrec":
-+    ctypedef struct poly "spolyrec":
-         poly *next
-         number *coef
-         unsigned long exp[1]
-@@ -630,9 +630,13 @@ cdef extern from "singular/Singular/libsingular.h":
-     # return p*q, destroys p and q
-     poly *p_Mult_q(poly *p, poly *q, ring *r)
- 
-+    # polynomial division, ignoring the rest
-+    # via singclap_pdivide resp. idLift, destroys p,q
-+    poly *p_Divide(poly *p, poly *q, ring *r)
-+
-     # divide monomial p by monomial q, p,q const
- 
--    poly *pDivide(poly *p,poly *q)
-+    poly *pMDivide(poly *p,poly *q)
- 
-     # return the i-th power of p; p destroyed, requires global ring
- 
-diff --git a/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx b/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx
-index 2a8d9ae021..aeff53af6c 100644
---- a/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx
-+++ b/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx
-@@ -190,8 +190,8 @@ from sage.libs.singular.decl cimport (
-     n_IsUnit, n_Invers,
-     p_ISet, rChangeCurrRing, p_Copy, p_Init, p_SetCoeff, p_Setm, p_SetExp, p_Add_q,
-     p_NSet, p_GetCoeff, p_Delete, p_GetExp, pNext, rRingVar, omAlloc0, omStrDup,
--    omFree, pDivide, p_SetCoeff0, n_Init, p_DivisibleBy, pLcm, p_LmDivisibleBy,
--    pDivide, p_IsConstant, p_ExpVectorEqual, p_String, p_LmInit, n_Copy,
-+    omFree, pMDivide, p_Divide, p_SetCoeff0, n_Init, p_DivisibleBy, pLcm, p_LmDivisibleBy,
-+    pMDivide, p_IsConstant, p_ExpVectorEqual, p_String, p_LmInit, n_Copy,
-     p_IsUnit, p_Series, p_Head, idInit, fast_map_common_subexp, id_Delete,
-     p_IsHomogeneous, p_Homogen, p_Totaldegree,pLDeg1_Totaldegree, singclap_pdivide, singclap_factorize,
-     idLift, IDELEMS, On, Off, SW_USE_CHINREM_GCD, SW_USE_EZGCD,
-@@ -1693,8 +1693,8 @@ cdef class MPolynomialRing_libsingular(MPolynomialRing_base):
-         if not g._poly:
-             raise ZeroDivisionError
- 
--        if r!=currRing: rChangeCurrRing(r)  # pDivide
--        res = pDivide(f._poly, g._poly)
-+        if r!=currRing: rChangeCurrRing(r)  # pMDivide
-+        res = pMDivide(f._poly, g._poly)
-         if coeff:
-             if r.cf.type == n_unknown or r.cf.cfDivBy(p_GetCoeff(f._poly, r), p_GetCoeff(g._poly, r), r.cf):
-                 n = r.cf.cfDiv( p_GetCoeff(f._poly, r) , p_GetCoeff(g._poly, r), r.cf)
-@@ -1853,8 +1853,8 @@ cdef class MPolynomialRing_libsingular(MPolynomialRing_base):
-                    and (<MPolynomial_libsingular>g) \
-                    and g.parent() is self \
-                    and p_LmDivisibleBy((<MPolynomial_libsingular>g)._poly, m, r):
--                if r!=currRing: rChangeCurrRing(r)  # pDivide
--                flt = pDivide(f._poly, (<MPolynomial_libsingular>g)._poly)
-+                if r!=currRing: rChangeCurrRing(r)  # pMDivide
-+                flt = pMDivide(f._poly, (<MPolynomial_libsingular>g)._poly)
-                 #p_SetCoeff(flt, n_Div( p_GetCoeff(f._poly, r) , p_GetCoeff((<MPolynomial_libsingular>g)._poly, r), r), r)
-                 p_SetCoeff(flt, n_Init(1, r), r)
-                 return new_MP(self,flt), g
-@@ -4023,16 +4023,6 @@ cdef class MPolynomial_libsingular(MPolynomial):
-             Traceback (most recent call last):
-             ...
-             NotImplementedError: Division of multivariate polynomials over non fields by non-monomials not implemented.
--
--        TESTS::
--
--            sage: P.<x,y> = ZZ[]
--            sage: p = 3*(-x^8*y^2 - x*y^9 + 6*x^8*y + 17*x^2*y^6 - x^3*y^2)
--            sage: q = 7*(x^2 + x*y + y^2 + 1)
--            sage: p*q//q == p
--            True
--            sage: p*q//p == q
--            True
-         """
-         cdef MPolynomialRing_libsingular parent = self._parent
-         cdef ring *r = self._parent_ring
-@@ -4052,13 +4042,18 @@ cdef class MPolynomial_libsingular(MPolynomial):
-         _right = <MPolynomial_libsingular>right
- 
-         if r.cf.type != n_unknown:
-+            if r.cf.type == n_Z:
-+                P = parent.change_ring(RationalField())
-+                f = P(self)//P(right)
-+                CM = list(f)
-+                return parent(sum([c.floor()*m for c,m in CM]))
-             if _right.is_monomial():
-                 p = _self._poly
-                 quo = p_ISet(0,r)
--                if r != currRing: rChangeCurrRing(r)   # pDivide
-+                if r != currRing: rChangeCurrRing(r)   # pMDivide
-                 while p:
-                     if p_DivisibleBy(_right._poly, p, r):
--                        temp = pDivide(p, _right._poly)
-+                        temp = pMDivide(p, _right._poly)
-                         p_SetCoeff0(temp, n_Copy(p_GetCoeff(p, r), r), r)
-                         quo = p_Add_q(quo, temp, r)
-                     p = pNext(p)
-@@ -4794,6 +4789,8 @@ cdef class MPolynomial_libsingular(MPolynomial):
-             sage: p = -x*y + x*z + 54*x - 2
-             sage: (5*p^2).lcm(3*p) == 15*p^2
-             True
-+            sage: lcm(2*x,2*x*y)
-+            2*x*y
-         """
-         cdef ring *_ring = self._parent_ring
-         cdef poly *ret
-@@ -4821,9 +4818,7 @@ cdef class MPolynomial_libsingular(MPolynomial):
-         if _ring!=currRing: rChangeCurrRing(_ring)  # singclap_gcd
-         gcd = singclap_gcd(p_Copy(self._poly, _ring), p_Copy(_g._poly, _ring), _ring )
-         prod = pp_Mult_qq(self._poly, _g._poly, _ring)
--        ret = singclap_pdivide(prod , gcd , _ring)
--        p_Delete(&prod, _ring)
--        p_Delete(&gcd, _ring)
-+        ret = p_Divide(prod, gcd, _ring)
-         if count >= 20:
-             sig_off()
-         return new_MP(self._parent, ret)
-@@ -4866,7 +4861,7 @@ cdef class MPolynomial_libsingular(MPolynomial):
-             sage: f.quo_rem(y)
-             (2*x^2, x + 1)
-             sage: f.quo_rem(3*x)
--            (2*x*y + 1, -4*x^2*y - 2*x + 1)
-+            (0, 2*x^2*y + x + 1)
- 
-         TESTS::
- 
-@@ -4888,7 +4883,7 @@ cdef class MPolynomial_libsingular(MPolynomial):
-         if right.is_zero():
-             raise ZeroDivisionError
- 
--        if not self._parent._base.is_field() and not is_IntegerRing(self._parent._base):
-+        if not self._parent._base.is_field():
-             py_quo = self//right
-             py_rem = self - right*py_quo
-             return py_quo, py_rem
-diff --git a/src/sage/rings/polynomial/plural.pyx b/src/sage/rings/polynomial/plural.pyx
-index d5439f7f08..ad20ebcca0 100644
---- a/src/sage/rings/polynomial/plural.pyx
-+++ b/src/sage/rings/polynomial/plural.pyx
-@@ -998,7 +998,7 @@ cdef class NCPolynomialRing_plural(Ring):
-         if not g._poly:
-             raise ZeroDivisionError
- 
--        res = pDivide(f._poly,g._poly)
-+        res = pMDivide(f._poly,g._poly)
-         if coeff:
-             if (r.cf.type == n_unknown) or r.cf.cfDivBy(p_GetCoeff(f._poly, r), p_GetCoeff(g._poly, r), r.cf):
-                 n = r.cf.cfDiv( p_GetCoeff(f._poly, r) , p_GetCoeff(g._poly, r), r.cf)
-@@ -1193,7 +1193,7 @@ cdef class NCPolynomialRing_plural(Ring):
-             if isinstance(g, NCPolynomial_plural) \
-                    and (<NCPolynomial_plural>g) \
-                    and p_LmDivisibleBy((<NCPolynomial_plural>g)._poly, m, r):
--                flt = pDivide(f._poly, (<NCPolynomial_plural>g)._poly)
-+                flt = pMDivide(f._poly, (<NCPolynomial_plural>g)._poly)
-                 #p_SetCoeff(flt, n_Div( p_GetCoeff(f._poly, r) , p_GetCoeff((<NCPolynomial_plural>g)._poly, r), r), r)
-                 p_SetCoeff(flt, n_Init(1, r), r)
-                 return new_NCP(self,flt), g
-diff --git a/src/sage/rings/polynomial/polynomial_singular_interface.py b/src/sage/rings/polynomial/polynomial_singular_interface.py
-index 9331169f8b..f753610fd3 100644
---- a/src/sage/rings/polynomial/polynomial_singular_interface.py
-+++ b/src/sage/rings/polynomial/polynomial_singular_interface.py
-@@ -81,8 +81,8 @@ class PolynomialRing_singular_repr:
-             sage: R.<x,y> = PolynomialRing(CC)
-             sage: singular(R)
-             polynomial ring, over a field, global ordering
--            //   coefficients: float[I](complex:15 digits, additional 0 digits)/(I^2+1)
--            //   number of vars : 2
-+            // coefficients: real[I](complex:15 digits, additional 0 digits)/(I^2+1)
-+            // number of vars : 2
-             //        block   1 : ordering dp
-             //                  : names    x y
-             //        block   2 : ordering C
-@@ -90,8 +90,8 @@ class PolynomialRing_singular_repr:
-             sage: R.<x,y> = PolynomialRing(RealField(100))
-             sage: singular(R)
-             polynomial ring, over a field, global ordering
--            //   coefficients: float
--            //   number of vars : 2
-+            // coefficients: Float()
-+            // number of vars : 2
-             //        block   1 : ordering dp
-             //                  : names    x y
-             //        block   2 : ordering C
diff --git a/pkgs/applications/science/math/sage/patches/spkg-scripts.patch b/pkgs/applications/science/math/sage/patches/spkg-scripts.patch
deleted file mode 100644
index 4d37998b288b..000000000000
--- a/pkgs/applications/science/math/sage/patches/spkg-scripts.patch
+++ /dev/null
@@ -1,46 +0,0 @@
-commit f02714d4aea80e17cb8df62bab75d7c1a1b61a8e
-Author: Timo Kaufmann <timokau@zoho.com>
-Date:   Mon Jul 9 18:26:18 2018 +0200
-
-    Don't attempt to create dirs when showing pkg info
-    
-    The script dir cannot be assumed to be writeable after installation.
-
-diff --git a/build/bin/sage-spkg b/build/bin/sage-spkg
-index f3e02aeae5..190d558ad1 100755
---- a/build/bin/sage-spkg
-+++ b/build/bin/sage-spkg
-@@ -167,14 +167,6 @@ if [ -z "$SAGE_BUILD_DIR" ]; then
-     export SAGE_BUILD_DIR="$SAGE_LOCAL/var/tmp/sage/build"
- fi
- 
--for dir in "$SAGE_SPKG_INST" "$SAGE_SPKG_SCRIPTS"; do
--    mkdir -p "$dir"
--    if [ $? -ne 0 ]; then
--        error_msg "Error creating directory $dir"
--        exit 1
--    fi
--done
--
- 
- # Remove '.' from PYTHONPATH, which may also come from SAGE_PATH, to avoid
- # trouble with setuptools / easy_install (cf. #10192, #10176):
-@@ -563,11 +555,13 @@ fi
- # Setup directories
- ##################################################################
- 
--mkdir -p "$SAGE_BUILD_DIR"
--if [ $? -ne 0 ]; then
--    error_msg "Error creating directory $SAGE_BUILD_DIR"
--    exit 1
--fi
-+for dir in "$SAGE_SPKG_INST" "$SAGE_SPKG_SCRIPTS" "$SAGE_BUILD_DIR"; do
-+    mkdir -p "$dir"
-+    if [ $? -ne 0 ]; then
-+        error_msg "Error creating directory $dir"
-+        exit 1
-+    fi
-+done
- 
- # Trac #5852: check write permissions
- if [ ! -w "$SAGE_BUILD_DIR" ]; then
diff --git a/pkgs/applications/science/math/sage/patches/test-in-tmpdir.patch b/pkgs/applications/science/math/sage/patches/test-in-tmpdir.patch
deleted file mode 100644
index febab3702771..000000000000
--- a/pkgs/applications/science/math/sage/patches/test-in-tmpdir.patch
+++ /dev/null
@@ -1,31 +0,0 @@
-diff --git a/src/sage/repl/ipython_kernel/install.py b/src/sage/repl/ipython_kernel/install.py
-index aa23c8405d..8a87de0591 100644
---- a/src/sage/repl/ipython_kernel/install.py
-+++ b/src/sage/repl/ipython_kernel/install.py
-@@ -112,7 +112,7 @@ class SageKernelSpec(object):
-         EXAMPLES::
- 
-             sage: from sage.repl.ipython_kernel.install import SageKernelSpec
--            sage: spec = SageKernelSpec()
-+            sage: spec = SageKernelSpec(prefix = tmp_dir())
-             sage: spec.use_local_mathjax()
-             sage: mathjax = os.path.join(spec.nbextensions_dir, 'mathjax')
-             sage: os.path.isdir(mathjax)
-@@ -129,7 +129,7 @@ class SageKernelSpec(object):
-         EXAMPLES::
- 
-             sage: from sage.repl.ipython_kernel.install import SageKernelSpec
--            sage: spec = SageKernelSpec()
-+            sage: spec = SageKernelSpec(prefix = tmp_dir())
-             sage: spec.use_local_jsmol()
-             sage: jsmol = os.path.join(spec.nbextensions_dir, 'jsmol')
-             sage: os.path.isdir(jsmol)
-@@ -146,7 +146,7 @@ class SageKernelSpec(object):
-         EXAMPLES::
- 
-             sage: from sage.repl.ipython_kernel.install import SageKernelSpec
--            sage: spec = SageKernelSpec()
-+            sage: spec = SageKernelSpec(prefix = tmp_dir())
-             sage: spec.use_local_threejs()
-             sage: threejs = os.path.join(spec.nbextensions_dir, 'threejs')
-             sage: os.path.isdir(threejs)
diff --git a/pkgs/applications/science/math/sage/sage-env.nix b/pkgs/applications/science/math/sage/sage-env.nix
index 74c2e0aa0360..317eb6e16c49 100644
--- a/pkgs/applications/science/math/sage/sage-env.nix
+++ b/pkgs/applications/science/math/sage/sage-env.nix
@@ -37,7 +37,7 @@
 , lcalc
 , rubiks
 , flintqs
-, openblasCompat
+, openblas-cblas-pc
 , flint
 , gmp
 , mpfr
@@ -98,9 +98,9 @@ writeTextFile rec {
     export PKG_CONFIG_PATH='${lib.concatStringsSep ":" (map (pkg: "${pkg}/lib/pkgconfig") [
         # This is only needed in the src/sage/misc/cython.py test and I'm not sure if there's really a use-case
         # for it outside of the tests. However since singular and openblas are runtime dependencies anyways
-        # it doesn't really hurt to include.
+        # and openblas-cblas-pc is tiny, it doesn't really hurt to include.
         singular
-        openblasCompat
+        openblas-cblas-pc
       ])
     }'
     export SAGE_ROOT='${sage-src}'
diff --git a/pkgs/applications/science/math/sage/sage-src.nix b/pkgs/applications/science/math/sage/sage-src.nix
index 7fd49fe205cc..f631fe38a5b0 100644
--- a/pkgs/applications/science/math/sage/sage-src.nix
+++ b/pkgs/applications/science/math/sage/sage-src.nix
@@ -3,35 +3,17 @@
 , fetchpatch
 }:
 stdenv.mkDerivation rec {
-  version = "8.3";
+  version = "8.4";
   name = "sage-src-${version}";
 
   src = fetchFromGitHub {
     owner = "sagemath";
     repo = "sage";
     rev = version;
-    sha256 = "0mbm99m5xry21xpi4q3q96gx392liwbifywf5awvl0j85a7rkfyx";
+    sha256 = "0gips1hagiz9m7s21bg5as8hrrm2x5k47h1bsq0pc46iplfwmv2d";
   };
 
   nixPatches = [
-    # https://trac.sagemath.org/ticket/25809
-    ./patches/spkg-scripts.patch
-
-    # https://trac.sagemath.org/ticket/25309
-    (fetchpatch {
-      name = "spkg-paths.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?h=97f06fddee920399d4fcda65aa9b0925774aec69&id=a86151429ccce1ddd085e8090ada8ebdf02f3310";
-      sha256 = "1xb9108rzzkdhn71vw44525620d3ww9jv1fph5a77v9y7nf9wgr7";
-    })
-    (fetchpatch {
-      name = "maxima-fas.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?h=97f06fddee920399d4fcda65aa9b0925774aec69";
-      sha256 = "14s50yg3hpw9cp3v581dx7zfmpm2j972im7x30iwki8k45mjvk3i";
-    })
-
-    # https://trac.sagemath.org/ticket/25722
-    ./patches/test-in-tmpdir.patch
-
     # https://trac.sagemath.org/ticket/25358
     (fetchpatch {
       name = "safe-directory-test-without-patch.patch";
@@ -46,45 +28,18 @@ stdenv.mkDerivation rec {
     # https://github.com/python/cpython/pull/7476
     ./patches/python-5755-hotpatch.patch
 
-    # https://trac.sagemath.org/ticket/25315
-    (fetchpatch {
-      name = "find-libraries-in-dyld-library-path.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?h=20d4593876ce9c6004eac2ab6fd61786d0d96a06";
-      sha256 = "1k3afq3qlzmgqwx6rzs5wv153vv9dsf5rk8pi61g57l3r3npbjmc";
-    })
+    # Revert the commit that made the sphinx build fork even in the single thread
+    # case. For some yet unknown reason, that breaks the docbuild on nix and archlinux.
+    # See https://groups.google.com/forum/#!msg/sage-packaging/VU4h8IWGFLA/mrmCMocYBwAJ.
+    ./patches/revert-sphinx-always-fork.patch
 
-    # https://trac.sagemath.org/ticket/25345
-    # (upstream patch doesn't apply on 8.2 source)
-    ./patches/dochtml-optional.patch
-
-    # work with pari with threads enabled at compile time (disable them at runtime)
-    # https://trac.sagemath.org/ticket/26002
-    ./patches/pari-no-threads.patch
+    # Make sure py2/py3 tests are only run when their expected context (all "sage"
+    # tests) are also run. That is necessary to test dochtml individually. See
+    # https://trac.sagemath.org/ticket/26110 for an upstream discussion.
+    ./patches/Only-test-py2-py3-optional-tests-when-all-of-sage-is.patch
   ];
 
   packageUpgradePatches = [
-    (fetchpatch {
-      name = "cypari2-1.2.1.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?h=62fe6eb15111327d930336d4252d5b23cbb22ab9";
-      sha256 = "1xax7vvs8h4xip16xcsp47xdb6lig6f2r3pl8cksvlz8lhgbyxh2";
-    })
-
-    # matplotlib 2.2.2 deprecated `normed` (replaced by `density`).
-    # This patch only ignores the warning. It would be equally easy to fix it
-    # (by replacing all mentions of `normed` by `density`), but its better to
-    # stay close to sage upstream. I didn't open an upstream ticket about it
-    # because the matplotlib update also requires a new dependency (kiwisolver)
-    # and I don't want to invest the time to learn how to add it.
-    ./patches/matplotlib-normed-deprecated.patch
-
-    # Update to 20171219 broke the doctests because of insignificant precision
-    # changes, make the doctests less fragile.
-    # I didn't open an upstream ticket because its not entirely clear if
-    # 20171219 is really "released" yet. It is listed on the github releases
-    # page, but not marked as "latest release" and the homepage still links to
-    # the last version.
-    ./patches/eclib-regulator-precision.patch
-
     # New glpk version has new warnings, filter those out until upstream sage has found a solution
     # https://trac.sagemath.org/ticket/24824
     ./patches/pari-stackwarn.patch # not actually necessary since tha pari upgrade, but necessary for the glpk patch to apply
@@ -94,27 +49,8 @@ stdenv.mkDerivation rec {
       stripLen = 1;
     })
 
-    # Only formatting changes.
     # https://trac.sagemath.org/ticket/25260
-    ./patches/numpy-1.14.3.patch
-
-    # https://trac.sagemath.org/ticket/25862
-    ./patches/eclib-20180710.patch
-
-    # https://trac.sagemath.org/ticket/24735
-    ./patches/singular-4.1.1p2.patch
-
-    # https://trac.sagemath.org/ticket/25567 and dependency #25635
-    (fetchpatch {
-      name = "pari-upgrade-dependency.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?id=6995e7cae1b3476ad0145f8dfc897cf91f0c3c4d";
-      sha256 = "1dvhabl1c9pwd9xkjvbjjg15mvb14b24p1f3cby1mlqk34d4lrs6";
-    })
-    (fetchpatch {
-      name = "pari-2.11.0.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?id=7af4748cab37d651eaa88be501db88f4a5ffc584";
-      sha256 = "13f740ly3c19gcmhjngiycvmc3mcfj61y00i6jv0wmfgpm2z3ank";
-    })
+    ./patches/numpy-1.15.1.patch
 
     # ntl upgrade
     (fetchpatch {
@@ -123,25 +59,11 @@ stdenv.mkDerivation rec {
       sha256 = "0p5wnvbx65i7cp0bjyaqgp4rly8xgnk12pqwaq3dqby0j2bk6ijb";
     })
 
-    # cddlib 0.94i -> 0.94j
-    (fetchpatch {
-      name = "cddlib-0.94j.patch";
-      url = "https://git.sagemath.org/sage.git/patch/?id=2ab1546b3e21d1d0ab3b4fcd58576848b3a2d888";
-      sha256 = "1c5gnasq7y9xxj762bn79bis0zi8d9bgg7jzlf64ifixsrc5cymb";
-    })
-
-    # arb 2.13.0 -> 2.14.0
-    (fetchpatch {
-      name = "arb-2.14.0.patch";
-      url = "https://git.sagemath.org/sage.git/patch?id2=8.4.beta0&id=8bef4fd2876a61969b516fe4eb3b8ad7cc076c5e";
-      sha256 = "00p3hfsfn3w2vxgd9fjd23mz7xfxjfravf8ysjxkyd657jbkpjmk";
-    })
-
-    # https://trac.sagemath.org/ticket/26117
+    # https://trac.sagemath.org/ticket/26360
     (fetchpatch {
-      name = "sympy-1.2.patch";
-      url = "https://git.sagemath.org/sage.git/patch?id2=8.4.beta2&id=d94a0a3a3fb4aec05a6f4d95166d90c284f05c36";
-      sha256 = "0an2xl1pp3jg36kgg2m1vb7sns7rprk1h3d0qy1gxwdab6i7qnvi";
+      name = "arb-2.15.1.patch";
+      url = "https://git.sagemath.org/sage.git/patch/?id=30cc778d46579bd0c7537ed33e8d7a4f40fd5c31";
+      sha256 = "13vc2q799dh745sm59xjjabllfj0sfjzcacf8k59kwj04x755d30";
     })
   ];
 
diff --git a/pkgs/applications/science/math/sage/sage-with-env.nix b/pkgs/applications/science/math/sage/sage-with-env.nix
index 8ccf8b5a4938..63b9772b8231 100644
--- a/pkgs/applications/science/math/sage/sage-with-env.nix
+++ b/pkgs/applications/science/math/sage/sage-with-env.nix
@@ -4,6 +4,9 @@
 , sage-env
 , sage-src
 , openblasCompat
+, openblas-blas-pc
+, openblas-cblas-pc
+, openblas-lapack-pc
 , pkg-config
 , three
 , singular
@@ -29,6 +32,9 @@ let
     makeWrapper
     pkg-config
     openblasCompat # lots of segfaults with regular (64 bit) openblas
+    openblas-blas-pc
+    openblas-cblas-pc
+    openblas-lapack-pc
     singular
     three
     pynac
diff --git a/pkgs/applications/science/math/sage/sage-wrapper.nix b/pkgs/applications/science/math/sage/sage-wrapper.nix
index 06b667f426fa..4b2f9c461c18 100644
--- a/pkgs/applications/science/math/sage/sage-wrapper.nix
+++ b/pkgs/applications/science/math/sage/sage-wrapper.nix
@@ -8,7 +8,7 @@
 
 stdenv.mkDerivation rec {
   version = sage.version;
-  name = "sage-wrapper-${version}";
+  name = "sage-${version}";
 
   buildInputs = [
     makeWrapper
diff --git a/pkgs/applications/science/math/sage/sage.nix b/pkgs/applications/science/math/sage/sage.nix
index b1e5d7278b0f..ad9a32e0ca56 100644
--- a/pkgs/applications/science/math/sage/sage.nix
+++ b/pkgs/applications/science/math/sage/sage.nix
@@ -5,7 +5,7 @@
 
 stdenv.mkDerivation rec {
   version = sage-with-env.version;
-  name = "sage-${version}";
+  name = "sage-tests-${version}";
 
   buildInputs = [
     makeWrapper
diff --git a/pkgs/applications/science/math/sage/sagelib.nix b/pkgs/applications/science/math/sage/sagelib.nix
index c1dbcf38304e..d26f5dad724e 100644
--- a/pkgs/applications/science/math/sage/sagelib.nix
+++ b/pkgs/applications/science/math/sage/sagelib.nix
@@ -3,6 +3,9 @@
 , buildPythonPackage
 , arb
 , openblasCompat
+, openblas-blas-pc
+, openblas-cblas-pc
+, openblas-lapack-pc
 , brial
 , cliquer
 , cypari2
@@ -44,6 +47,8 @@
 , singular
 , pip
 , jupyter_core
+, libhomfly
+, libbraiding
 }:
 
 buildPythonPackage rec {
@@ -56,7 +61,9 @@ buildPythonPackage rec {
   nativeBuildInputs = [
     iml
     perl
-    openblasCompat
+    openblas-blas-pc
+    openblas-cblas-pc
+    openblas-lapack-pc
     jupyter_core
   ];
 
@@ -104,6 +111,8 @@ buildPythonPackage rec {
     pip
     cython
     cysignals
+    libhomfly
+    libbraiding
   ];
 
   buildPhase = ''
diff --git a/pkgs/applications/science/misc/root/5.nix b/pkgs/applications/science/misc/root/5.nix
new file mode 100644
index 000000000000..7f43dfb328a8
--- /dev/null
+++ b/pkgs/applications/science/misc/root/5.nix
@@ -0,0 +1,77 @@
+{ stdenv, fetchurl, cmake, pcre, pkgconfig, python2
+, libX11, libXpm, libXft, libXext, libGLU_combined, zlib, libxml2, lzma, gsl_1
+, Cocoa, OpenGL, noSplash ? false }:
+
+stdenv.mkDerivation rec {
+  name = "root-${version}";
+  version = "5.34.36";
+
+  src = fetchurl {
+    url = "https://root.cern.ch/download/root_v${version}.source.tar.gz";
+    sha256 = "1kbx1jxc0i5xfghpybk8927a0wamxyayij9c74zlqm0595gqx1pw";
+  };
+
+  nativeBuildInputs = [ pkgconfig ];
+  buildInputs = [ cmake pcre python2 zlib libxml2 lzma gsl_1 ]
+    ++ stdenv.lib.optionals (!stdenv.isDarwin) [ libX11 libXpm libXft libXext libGLU_combined ]
+    ++ stdenv.lib.optionals (stdenv.isDarwin) [ Cocoa OpenGL ]
+    ;
+
+  patches = [
+    ./sw_vers_root5.patch
+  ];
+
+  preConfigure = ''
+    patchShebangs build/unix/
+    ln -s ${stdenv.lib.getDev stdenv.cc.libc}/include/AvailabilityMacros.h cint/cint/include/
+  '' + stdenv.lib.optionalString noSplash ''
+    substituteInPlace rootx/src/rootx.cxx --replace "gNoLogo = false" "gNoLogo = true"
+  '';
+
+  cmakeFlags = [
+    "-Drpath=ON"
+    "-DCMAKE_INSTALL_LIBDIR=lib"
+    "-DCMAKE_INSTALL_INCLUDEDIR=include"
+    "-Dalien=OFF"
+    "-Dbonjour=OFF"
+    "-Dcastor=OFF"
+    "-Dchirp=OFF"
+    "-Ddavix=OFF"
+    "-Ddcache=OFF"
+    "-Dfftw3=OFF"
+    "-Dfitsio=OFF"
+    "-Dfortran=OFF"
+    "-Dgfal=OFF"
+    "-Dgsl_shared=ON"
+    "-Dgviz=OFF"
+    "-Dhdfs=OFF"
+    "-Dkrb5=OFF"
+    "-Dldap=OFF"
+    "-Dmathmore=ON"
+    "-Dmonalisa=OFF"
+    "-Dmysql=OFF"
+    "-Dodbc=OFF"
+    "-Dopengl=ON"
+    "-Doracle=OFF"
+    "-Dpgsql=OFF"
+    "-Dpythia6=OFF"
+    "-Dpythia8=OFF"
+    "-Drfio=OFF"
+    "-Dsqlite=OFF"
+    "-Dssl=OFF"
+    "-Dxml=ON"
+    "-Dxrootd=OFF"
+  ]
+  ++ stdenv.lib.optional stdenv.isDarwin "-DOPENGL_INCLUDE_DIR=${OpenGL}/Library/Frameworks";
+
+  enableParallelBuilding = true;
+
+  setupHook = ./setup-hook.sh;
+
+  meta = with stdenv.lib; {
+    homepage = https://root.cern.ch/;
+    description = "A data analysis framework";
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ veprbl ];
+  };
+}
diff --git a/pkgs/applications/science/misc/root/default.nix b/pkgs/applications/science/misc/root/default.nix
index e966e798ae6d..2ec1ded68a26 100644
--- a/pkgs/applications/science/misc/root/default.nix
+++ b/pkgs/applications/science/misc/root/default.nix
@@ -67,10 +67,11 @@ stdenv.mkDerivation rec {
 
   setupHook = ./setup-hook.sh;
 
-  meta = {
+  meta = with stdenv.lib; {
     homepage = https://root.cern.ch/;
     description = "A data analysis framework";
-    platforms = stdenv.lib.platforms.unix;
-    maintainers = with stdenv.lib.maintainers; [ veprbl ];
+    platforms = platforms.unix;
+    maintainers = [ maintainers.veprbl ];
+    license = licenses.lgpl21;
   };
 }
diff --git a/pkgs/applications/science/misc/root/sw_vers_root5.patch b/pkgs/applications/science/misc/root/sw_vers_root5.patch
new file mode 100644
index 000000000000..f044bed91f3d
--- /dev/null
+++ b/pkgs/applications/science/misc/root/sw_vers_root5.patch
@@ -0,0 +1,104 @@
+diff --git a/build/unix/compiledata.sh b/build/unix/compiledata.sh
+--- a/build/unix/compiledata.sh
++++ b/build/unix/compiledata.sh
+@@ -49,7 +49,7 @@ fi
+ 
+ if [ "$ARCH" = "macosx" ] || [ "$ARCH" = "macosx64" ] || \
+    [ "$ARCH" = "macosxicc" ]; then
+-   macosx_minor=`sw_vers | sed -n 's/ProductVersion://p' | cut -d . -f 2`
++   macosx_minor=7
+    SOEXT="so"
+    if [ $macosx_minor -ge 5 ]; then
+       if [ "x`echo $SOFLAGS | grep -- '-install_name'`" != "x" ]; then
+diff --git a/cmake/modules/SetUpMacOS.cmake b/cmake/modules/SetUpMacOS.cmake
+--- a/cmake/modules/SetUpMacOS.cmake
++++ b/cmake/modules/SetUpMacOS.cmake
+@@ -12,25 +12,11 @@ set(CMAKE_PREFIX_PATH ${CMAKE_PREFIX_PATH} /usr/X11R6)
+ #---------------------------------------------------------------------------------------------------------
+ 
+ if (CMAKE_SYSTEM_NAME MATCHES Darwin)
+-  EXECUTE_PROCESS(COMMAND sw_vers "-productVersion"
+-                  COMMAND cut -d . -f 1-2
+-                  OUTPUT_VARIABLE MACOSX_VERSION OUTPUT_STRIP_TRAILING_WHITESPACE)
+-  MESSAGE(STATUS "Found a Mac OS X System ${MACOSX_VERSION}")
+-  EXECUTE_PROCESS(COMMAND sw_vers "-productVersion"
+-                  COMMAND cut -d . -f 2
+-                  OUTPUT_VARIABLE MACOSX_MINOR OUTPUT_STRIP_TRAILING_WHITESPACE)
+-
+-  if(MACOSX_VERSION VERSION_GREATER 10.7 AND ${CMAKE_CXX_COMPILER_ID} STREQUAL Clang)
+     set(libcxx ON CACHE BOOL "Build using libc++" FORCE)
+-  endif()
+ 
+-  if(${MACOSX_MINOR} GREATER 4)
+     #TODO: check haveconfig and rpath -> set rpath true
+     #TODO: check Thread, define link command
+     #TODO: more stuff check configure script
+-    execute_process(COMMAND /usr/sbin/sysctl machdep.cpu.extfeatures OUTPUT_VARIABLE SYSCTL_OUTPUT)
+-    if(${SYSCTL_OUTPUT} MATCHES 64)
+-       MESSAGE(STATUS "Found a 64bit system")
+        set(ROOT_ARCHITECTURE macosx64)
+        SET(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS}")
+        SET(CMAKE_SHARED_LIBRARY_CREATE_C_FLAGS "${CMAKE_SHARED_LIBRARY_CREATE_C_FLAGS} -m64")
+@@ -38,28 +24,6 @@ if (CMAKE_SYSTEM_NAME MATCHES Darwin)
+        SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m64")
+        SET(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -m64")
+        SET(CMAKE_FORTRAN_FLAGS "${CMAKE_FORTRAN_FLAGS} -m64")
+-    else(${SYSCTL_OUTPUT} MATCHES 64)
+-       MESSAGE(STATUS "Found a 32bit system")
+-       SET(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m32")
+-       SET(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -m32")
+-       SET(CMAKE_FORTRAN_FLAGS "${CMAKE_FORTRAN_FLAGS} -m32")
+-    endif(${SYSCTL_OUTPUT} MATCHES 64)
+-  endif()
+-
+-  if(MACOSX_VERSION VERSION_GREATER 10.6)
+-    set(MACOSX_SSL_DEPRECATED ON)
+-  endif()
+-  if(MACOSX_VERSION VERSION_GREATER 10.7)
+-    set(MACOSX_ODBC_DEPRECATED ON)
+-  endif()
+-  if(MACOSX_VERSION VERSION_GREATER 10.8)
+-    set(MACOSX_GLU_DEPRECATED ON)
+-    set(MACOSX_KRB5_DEPRECATED ON)
+-    set(MACOSX_TMPNAM_DEPRECATED ON)
+-  endif()
+-  if(MACOSX_VERSION VERSION_GREATER 10.9)
+-    set(MACOSX_LDAP_DEPRECATED ON)
+-  endif()
+ 
+   if (CMAKE_COMPILER_IS_GNUCXX)
+      message(STATUS "Found GNU compiler collection")
+@@ -132,7 +96,7 @@ if (CMAKE_SYSTEM_NAME MATCHES Darwin)
+   endif()
+ 
+   #---Set Linker flags----------------------------------------------------------------------
+-  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS}  -mmacosx-version-min=${MACOSX_VERSION} -Wl,-rpath,@loader_path/../lib")
++  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath,@loader_path/../lib")
+ 
+ 
+ else (CMAKE_SYSTEM_NAME MATCHES Darwin)
+diff --git a/config/root-config.in b/config/root-config.in
+--- a/config/root-config.in
++++ b/config/root-config.in
+@@ -391,7 +391,7 @@ macosxicc)
+    ;;
+ macosx64)
+    # MacOS X with gcc (GNU cc v4.x) in 64 bit mode
+-   macosx_minor=`sw_vers | sed -n 's/ProductVersion://p' | cut -d . -f 2`
++   macosx_minor=7
+    # cannot find the one linked to libGraf if relocated after built
+    if [ $macosx_minor -le 4 ]; then
+       rootlibs="$rootlibs -lfreetype"
+diff --git a/cint/ROOT/CMakeLists.txt b/cint/ROOT/CMakeLists.txt
+--- a/cint/ROOT/CMakeLists.txt
++++ b/cint/ROOT/CMakeLists.txt
+@@ -232,9 +232,7 @@ foreach(_name ${CINTINCDLLNAMES})
+                        DEPENDS ${HEADER_OUTPUT_PATH}/systypes.h
+                       )
+
+-    if(MACOSX_MINOR GREATER 4)
+       set(_ExtraFlag "-D__DARWIN_UNIX03")
+-    endif()
+
+     add_custom_command(OUTPUT ${OutFileName}
+                        COMMAND cint_tmp -K -w1 -z${_name} -n${OutFileName} -D__MAKECINT__ -DG__MAKECINT ${_ExtraFlag} -c-2 -Z0 ${InFileName} ${AdditionalHeaderFiles} ${CMAKE_BINARY_DIR}/cint/cint/include/sys/types.h ${CMAKE_SOURCE_DIR}/cint/cint/lib/posix/posix.h
\ No newline at end of file
diff --git a/pkgs/applications/science/misc/sasview/default.nix b/pkgs/applications/science/misc/sasview/default.nix
index bad29df9dc88..ed6fa3ae886b 100644
--- a/pkgs/applications/science/misc/sasview/default.nix
+++ b/pkgs/applications/science/misc/sasview/default.nix
@@ -17,7 +17,7 @@ in
 
 python.pkgs.buildPythonApplication rec {
   pname = "sasview";
-  version = "unstable-2018-05-05";
+  version = "4.2.0";
 
   checkInputs = with python.pkgs; [
     pytest
@@ -60,8 +60,8 @@ python.pkgs.buildPythonApplication rec {
   src = fetchFromGitHub {
     owner = "SasView";
     repo = "sasview";
-    rev = "de431924d0ddf73cfb952df88bd6661181947019";
-    sha256 = "01bk0i0g65yzyq16n1a61rgjna8rrc2i51x2ndf1z7khb1fl16vg";
+    rev = "v${version}";
+    sha256 = "0k3486h46k6406h0vla8h68fd78wh3dcaq5w6f12jh6g4cjxv9qa";
   };
 
   patches = [ ./pyparsing-fix.patch ./local_config.patch ];
diff --git a/pkgs/applications/science/misc/snakemake/default.nix b/pkgs/applications/science/misc/snakemake/default.nix
index 6b0570814f2b..6f04d436877f 100644
--- a/pkgs/applications/science/misc/snakemake/default.nix
+++ b/pkgs/applications/science/misc/snakemake/default.nix
@@ -37,5 +37,6 @@ python.buildPythonPackage rec {
       workflows are essentially Python scripts extended by declarative code to define
       rules. Rules describe how to create output files from input files.
     '';
+    maintainers = with maintainers; [ helkafen renatoGarcia ];
   };
 }
diff --git a/pkgs/applications/science/molecular-dynamics/gromacs/default.nix b/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
index 295e726c679d..1caa84a69334 100644
--- a/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
+++ b/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
@@ -8,11 +8,11 @@
 
 
 stdenv.mkDerivation {
-  name = "gromacs-2018.2";
+  name = "gromacs-2018.3";
 
   src = fetchurl {
-    url = "ftp://ftp.gromacs.org/pub/gromacs/gromacs-2018.2.tar.gz";
-    sha256 = "0mvqsg2j4h529a0vvvgpa4cb3p8zan18zcdlmx1na2si1h9fipab";
+    url = "ftp://ftp.gromacs.org/pub/gromacs/gromacs-2018.3.tar.gz";
+    sha256 = "14d219987h98mv5xgn2846snmslwax8z3cgp5b2njacp4j9a88s4";
   };
 
   buildInputs = [cmake fftw]
diff --git a/pkgs/applications/science/physics/xfitter/calling_convention.patch b/pkgs/applications/science/physics/xfitter/calling_convention.patch
new file mode 100644
index 000000000000..5b216b6e0928
--- /dev/null
+++ b/pkgs/applications/science/physics/xfitter/calling_convention.patch
@@ -0,0 +1,355 @@
+diff --git a/DY/src/finterface.cc b/DY/src/finterface.cc
+index 0405786..eb171d0 100644
+--- a/DY/src/finterface.cc
++++ b/DY/src/finterface.cc
+@@ -14,17 +14,17 @@
+ using namespace std;
+ 
+ extern "C" {
+-  int dy_create_calc_(const int *ds_id, const int *chg_prod, 
++  void dy_create_calc_(const int *ds_id, const int *chg_prod, 
+       const double *beam_en, const char *boz,
+       const double *ranges, const char *var_name, 
+       const int *n_bins, const double *bin_edges);
+ 
+-  int dy_do_calc_();
++  void dy_do_calc_();
+ 
+-  int dy_get_res_(const int *ds_id, double *calc_res);
++  void dy_get_res_(const int *ds_id, double *calc_res);
+ 
+   int dy_release_();
+-  int dy_set_ewpars_();
++  void dy_set_ewpars_();
+ }
+ 
+ typedef map <int, DYcalc* > DCmap;
+@@ -34,7 +34,7 @@ vector<BinMatrix*> gBinMatrices;
+ 
+ // initializes Drell-Yan LO calculations with info on
+ // beam, process, kinematic cuts, and bins.
+-int dy_create_calc_(const int *ds_id, const int *chg_prod, 
++void dy_create_calc_(const int *ds_id, const int *chg_prod, 
+     const double *beam_en, const char *boz,
+     const double *ranges, const char *var_name, 
+     const int *n_bins, const double *bin_edges)
+@@ -99,13 +99,11 @@ int dy_create_calc_(const int *ds_id, const int *chg_prod,
+   // create calculator and put to map
+   DYcalc * dc = new DYcalc(bm, pc, int_steps);
+   gCalcs.insert( pair<int,DYcalc*>( *ds_id,dc ) );
+-
+-  return 1;
+ }
+ 
+ 
+ // calculate Drell-Yan LO cross sections for all data sets
+-int dy_do_calc_()
++void dy_do_calc_()
+ {
+   // evolve convolutions
+   vector<PDFconv*>::iterator ipc = gPDFconvs.begin();
+@@ -118,24 +116,20 @@ int dy_do_calc_()
+     if ( true != idc->second->Integrate() ) {
+       cout << "Something is wrong with DY integration for " 
+            << idc->first << " data set." << endl;
+-      return 0;
++      return;
+     }
+   }
+-
+-  return 1;
+ }
+ 
+ 
+ // return DY calculations for data set ds_name
+-int dy_get_res_(const int *ds_id, double *calc_res)
++void dy_get_res_(const int *ds_id, double *calc_res)
+ {
+   DYcalc * dc = gCalcs.find(*ds_id)->second;
+   dc->getCalcRes(calc_res);
+-
+-  return 1;
+ }
+ 
+-int dy_set_ewpars_(){
++void dy_set_ewpars_(){
+   PhysPar::setPhysPar();
+ }
+ 
+@@ -155,6 +149,4 @@ int dy_release_()
+   for (; idc != gCalcs.end() ; idc++){
+     delete (idc->second);
+   }
+-
+-  return 1;
+ }
+diff --git a/FastNLO/src/FastNLOInterface.cc b/FastNLO/src/FastNLOInterface.cc
+index 20f8a75..a6dac79 100644
+--- a/FastNLO/src/FastNLOInterface.cc
++++ b/FastNLO/src/FastNLOInterface.cc
+@@ -39,14 +39,14 @@ void gauleg(double x1,double x2,double *x,double *w, int n);
+ 
+ 
+ extern "C" {
+-  int fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_FIT_ORDER, bool *PublicationUnits , double* murdef, double* murscale, double *mufdef, double* mufscale);
+-  int fastnlocalc_(const int *idataset, double *xsec);
+-  int fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *tot, int *Npt);
+-  int fastnlopointskip_(const int *idataset, int *point, int *npoints);
+-  int hf_errlog_(const int* ID, const char* TEXT, long length);
+-  int hf_stop_();
++  void fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_FIT_ORDER, bool *PublicationUnits , double* murdef, double* murscale, double *mufdef, double* mufscale);
++  void fastnlocalc_(const int *idataset, double *xsec);
++  void fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *tot, int *Npt);
++  void fastnlopointskip_(const int *idataset, int *point, int *npoints);
++  void hf_errlog_(const int* ID, const char* TEXT, long length);
++  void hf_stop_();
+   double interp_(double *A, double *xx1, double *x, int *NGrid1, double *res);
+-  int setfastnlotoppar_(const int *idataset);
++  void setfastnlotoppar_(const int *idataset);
+ }
+ 
+ 
+@@ -58,7 +58,7 @@ map<int, FastNLOxFitter*> gFastNLO_array;
+ map<int, BoolArray*>     gUsedPoints_array;
+ int CreateUsedPointsArray(int idataset, int npoints);
+ 
+-int fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_FIT_ORDER, bool *PublicationUnits , double* murdef, double* murscale, double *mufdef, double* mufscale) {
++void fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_FIT_ORDER, bool *PublicationUnits , double* murdef, double* murscale, double *mufdef, double* mufscale) {
+ 
+   
+    map<int, FastNLOxFitter*>::const_iterator FastNLOIterator = gFastNLO_array.find(*idataset);
+@@ -67,7 +67,7 @@ int fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_
+      const char* text = "I: Double initialization of the same fastnlo data set!";
+      hf_errlog_(&id, text, (long)strlen(text));
+      //hf_stop_();
+-     return 1;
++     return;
+    }
+    
+    FastNLOxFitter* fnloreader = new FastNLOxFitter( thfile );  
+@@ -112,10 +112,9 @@ int fastnloinit_(const char *s, const int *idataset, const char *thfile, int *I_
+    }
+    
+    gFastNLO_array.insert(pair<int, FastNLOxFitter*>(*idataset, fnloreader) );
+-   return 0;
+ }
+ 
+-int setfastnlotoppar_(const int *idataset) {
++void setfastnlotoppar_(const int *idataset) {
+    //!< Dedicated settings for difftop
+    map<int, FastNLOxFitter*>::const_iterator FastNLOIterator = gFastNLO_array.find(*idataset);
+    map<int, BoolArray*>::const_iterator UsedPointsIterator = gUsedPoints_array.find(*idataset);
+@@ -130,11 +129,9 @@ int setfastnlotoppar_(const int *idataset) {
+    fnloreader->SetExternalFuncForMuF( &Function_Mu );
+    fnloreader->SetExternalFuncForMuR( &Function_Mu);
+    //fnloreader->SetScaleFactorsMuRMuF(1.0,1.0); //Be reminded that muR and muF scales are hard coded (that's not true!)
+-
+-   return 0;
+ }
+ 
+-int fastnlocalc_(const int *idataset, double *xsec) {
++void fastnlocalc_(const int *idataset, double *xsec) {
+   
+    map<int, FastNLOxFitter*>::const_iterator FastNLOIterator = gFastNLO_array.find(*idataset);
+    map<int, BoolArray*>::const_iterator UsedPointsIterator = gUsedPoints_array.find(*idataset);
+@@ -176,13 +173,10 @@ int fastnlocalc_(const int *idataset, double *xsec) {
+        outputidx++;
+      }
+    }
+- 
+-
+-   return 0;
+ }
+ 
+ //MK14 New function for Difftop calculation: it is called in trunk/src/difftop_fastnlo.f
+-int fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *tot, int *Npt){
++void fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *tot, int *Npt){
+   
+    map<int, FastNLOxFitter*>::const_iterator FastNLOIterator = gFastNLO_array.find(*idataset);
+    map<int, BoolArray*>::const_iterator UsedPointsIterator = gUsedPoints_array.find(*idataset);
+@@ -262,10 +256,6 @@ int fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *to
+      Total += interpC(xsec,xg[k],thbin,Nthpoints)*wg[k];
+ 
+    *tot = Total;
+-
+-
+-
+-   return 0;
+ }
+ 
+ 
+@@ -277,7 +267,7 @@ int fastnlocalctop_(const int *idataset, double *xsec, double *thbin, double *to
+ 
+ 
+ 
+-int fastnlopointskip_(const int *idataset, int *point, int *npoints) {
++void fastnlopointskip_(const int *idataset, int *point, int *npoints) {
+   map<int, BoolArray*>::const_iterator UsedPointsIterator = gUsedPoints_array.find(*idataset);
+   if(UsedPointsIterator == gUsedPoints_array.end( )) 
+     CreateUsedPointsArray(*idataset, *npoints);
+@@ -292,8 +282,6 @@ int fastnlopointskip_(const int *idataset, int *point, int *npoints) {
+   
+   BoolArray*     usedpoints = UsedPointsIterator->second;
+   usedpoints->at(*point-1) = false;
+-
+-  return 0;
+ }
+ 
+ int CreateUsedPointsArray(int idataset, int npoints) {
+diff --git a/Hathor/src/HathorInterface.cc b/Hathor/src/HathorInterface.cc
+index 7da88b1..96576a3 100644
+--- a/Hathor/src/HathorInterface.cc
++++ b/Hathor/src/HathorInterface.cc
+@@ -6,9 +6,9 @@
+ #include "../interface/xFitterPdf.h"
+ 
+ extern "C" {
+-  int hathorinit_(const int* idataset, const double& sqrtS, const bool& ppbar, const double& mt,
++  void hathorinit_(const int* idataset, const double& sqrtS, const bool& ppbar, const double& mt,
+ 		  const unsigned int& pertubOrder, const unsigned int& precisionLevel);
+-  int hathorcalc_(const int *idataset, double *xsec);
++  void hathorcalc_(const int *idataset, double *xsec);
+ }
+ 
+ extern "C" {
+@@ -19,7 +19,7 @@ extern "C" {
+ }
+ 
+ extern "C" {
+-  int hf_errlog_(const int* ID, const char* TEXT, long length);
++  void hf_errlog_(const int* ID, const char* TEXT, long length);
+ }
+ 
+ // FIXME: delete pointers at the end! (in some hathordestroy_ or so)
+@@ -28,7 +28,7 @@ xFitterPdf* pdf;
+ int* rndStore;
+ double mtop;
+ 
+-int hathorinit_(const int* idataset, const double& sqrtS, const bool& ppbar, const double& mt,
++void hathorinit_(const int* idataset, const double& sqrtS, const bool& ppbar, const double& mt,
+ 		const unsigned int& pertubOrder, const unsigned int& precisionLevel) {
+ 
+   if(hathor_array.size()==0) {
+@@ -69,7 +69,7 @@ int hathorinit_(const int* idataset, const double& sqrtS, const bool& ppbar, con
+   return 0;
+ }
+ 
+-int hathorcalc_(const int *idataset, double *xsec) {
++void hathorcalc_(const int *idataset, double *xsec) {
+   rlxd_reset(rndStore);
+ 
+   std::map<int, Hathor*>::const_iterator hathorIter = hathor_array.find(*idataset);
+diff --git a/src/ftheor_eval.cc b/src/ftheor_eval.cc
+index 1dd4e8b..8bc7991 100644
+--- a/src/ftheor_eval.cc
++++ b/src/ftheor_eval.cc
+@@ -19,15 +19,15 @@
+ using namespace std;
+ 
+ extern "C" {
+-  int set_theor_eval_(int *dsId);//, int *nTerms, char **TermName, char **TermType, 
++  void set_theor_eval_(int *dsId);//, int *nTerms, char **TermName, char **TermType, 
+ //    char **TermSource, char *TermExpr);
+-  int set_theor_bins_(int *dsId, int *nBinDimension, int *nPoints, int *binFlags, 
++  void set_theor_bins_(int *dsId, int *nBinDimension, int *nPoints, int *binFlags, 
+     double *allBins);
+ //  int set_theor_units_(int *dsId, double *units);
+-  int init_theor_eval_(int *dsId);
+-  int update_theor_ckm_();
+-  int get_theor_eval_(int *dsId, int* np, int* idx);
+-  int close_theor_eval_();
++  void init_theor_eval_(int *dsId);
++  void update_theor_ckm_();
++  void get_theor_eval_(int *dsId, int* np, int* idx);
++  void close_theor_eval_();
+ }
+ 
+ /// global dataset to theory evaluation pointer map
+@@ -59,7 +59,7 @@ extern struct ord_scales {
+  dataset ID.
+  write details on argumets
+  */
+-int set_theor_eval_(int *dsId)//, int *nTerms, char **TermName, char **TermType, 
++void set_theor_eval_(int *dsId)//, int *nTerms, char **TermName, char **TermType, 
+ //  char **TermSource, char *TermExpr)
+ {
+   // convert fortran strings to c++
+@@ -90,15 +90,13 @@ int set_theor_eval_(int *dsId)//, int *nTerms, char **TermName, char **TermType,
+     << " already exists." << endl;
+     exit(1); // make proper exit later
+   }
+-
+-  return 1;
+ }
+ 
+ /*!
+  Sets datasets bins in theory evaluations.
+  write details on argumets
+  */
+-int set_theor_bins_(int *dsId, int *nBinDimension, int *nPoints, int *binFlags, 
++void set_theor_bins_(int *dsId, int *nBinDimension, int *nPoints, int *binFlags, 
+   double *allBins)
+ {
+   tTEmap::iterator it = gTEmap.find(*dsId);
+@@ -110,7 +108,6 @@ int set_theor_bins_(int *dsId, int *nBinDimension, int *nPoints, int *binFlags,
+   
+   TheorEval *te = gTEmap.at(*dsId);
+   te->setBins(*nBinDimension, *nPoints, binFlags, allBins);
+-  return 1;
+ }
+ 
+ /*
+@@ -132,7 +129,7 @@ int set_theor_units_(int *dsId, double *units)
+ /*!
+  Initializes theory for requested dataset.
+  */
+-int init_theor_eval_(int *dsId)
++void init_theor_eval_(int *dsId)
+ {
+   tTEmap::iterator it = gTEmap.find(*dsId);
+   if (it == gTEmap.end() ) { 
+@@ -148,7 +145,7 @@ int init_theor_eval_(int *dsId)
+ /*!
+  Updates the CKM matrix to all the initialized appl grids
+  */
+-int update_theor_ckm_()
++void update_theor_ckm_()
+ {
+   double a_ckm[] = { ckm_matrix_.Vud, ckm_matrix_.Vus, ckm_matrix_.Vub,
+                                   ckm_matrix_.Vcd, ckm_matrix_.Vcs, ckm_matrix_.Vcb,
+@@ -164,7 +161,7 @@ int update_theor_ckm_()
+ /*!
+  Evaluates theory for requested dataset and writes it to the global THEO array.
+  */
+-int get_theor_eval_(int *dsId, int *np, int*idx)
++void get_theor_eval_(int *dsId, int *np, int*idx)
+ {
+ 
+   tTEmap::iterator it = gTEmap.find(*dsId);
+@@ -194,11 +191,11 @@ int get_theor_eval_(int *dsId, int *np, int*idx)
+   // write the predictions to THEO array
+   if( ip != *np ){
+     cout << "ERROR in get_theor_eval_: number of points mismatch" << endl;
+-    return -1;
++    return;
+   }
+ }
+ 
+-int close_theor_eval_()
++void close_theor_eval_()
+ {
+   tTEmap::iterator it = gTEmap.begin();
+   for (; it!= gTEmap.end(); it++){
+diff --git a/src/lhapdf6_output.c b/src/lhapdf6_output.c
+index 4b20b68..549c521 100644
+--- a/src/lhapdf6_output.c
++++ b/src/lhapdf6_output.c
+@@ -64,7 +64,7 @@ extern double bvalij_(int *,int *,int *,int *,int *);
+ extern double bvalxq_(int *,int *,double *,double *,int *);

+ extern double hf_get_alphas_(double *);

+ extern int getord_(int *);

+-extern int grpars_(int *, double *, double *, int *, double *, double *, int *);

++extern void grpars_(int *, double *, double *, int *, double *, double *, int *);

+ extern int getcbt_(int *, double *, double *, double *);

+ extern void getpdfunctype_heraf_(int *mc, int *asymh, int *symh, char *name, size_t size);

+ extern void hf_errlog_(int *, char *, size_t);

diff --git a/pkgs/applications/science/physics/xfitter/default.nix b/pkgs/applications/science/physics/xfitter/default.nix
new file mode 100644
index 000000000000..a6ec9960045d
--- /dev/null
+++ b/pkgs/applications/science/physics/xfitter/default.nix
@@ -0,0 +1,54 @@
+{ stdenv, fetchurl, apfel, apfelgrid, applgrid, blas, gfortran, lhapdf, liblapackWithoutAtlas, libyaml, lynx, mela, root5, qcdnum, which }:
+
+stdenv.mkDerivation rec {
+  name = "xfitter-${version}";
+  version = "2.0.0";
+
+  src = fetchurl {
+    name = "${name}.tgz";
+    url = "https://www.xfitter.org/xFitter/xFitter/DownloadPage?action=AttachFile&do=get&target=${name}.tgz";
+    sha256 = "0j47s8laq3aqjlgp769yicvgyzqjb738a3rqss51d9fjrihi2515";
+  };
+
+  patches = [
+    ./calling_convention.patch
+  ];
+
+  preConfigure =
+  # Fix F77LD to workaround for a following build error:
+  #
+  #   gfortran: error: unrecognized command line option '-stdlib=libc++'
+  #
+    stdenv.lib.optionalString stdenv.isDarwin ''
+      substituteInPlace src/Makefile.in \
+        --replace "F77LD = \$(F77)" "F77LD = \$(CXXLD)" \
+    '';
+
+  configureFlags = [
+    "--enable-apfel"
+    "--enable-apfelgrid"
+    "--enable-applgrid"
+    "--enable-mela"
+    "--enable-lhapdf"
+  ];
+
+  nativeBuildInputs = [ gfortran which ];
+  buildInputs =
+    [ apfel apfelgrid applgrid blas lhapdf liblapackWithoutAtlas mela root5 qcdnum ]
+    # pdf2yaml requires fmemopen and open_memstream which are not readily available on Darwin
+    ++ stdenv.lib.optional (!stdenv.isDarwin) libyaml
+    ;
+  propagatedBuildInputs = [ lynx ];
+
+  enableParallelBuilding = true;
+
+  hardeningDisable = [ "format" ];
+
+  meta = with stdenv.lib; {
+    description = "The xFitter project is an open source QCD fit framework ready to extract PDFs and assess the impact of new data";
+    license     = licenses.gpl3;
+    homepage    = https://www.xfitter.org/xFitter;
+    platforms   = platforms.unix;
+    maintainers = with maintainers; [ veprbl ];
+  };
+}