coqPackages.mathcomp,ssreflect: 1.5 -> 1.6

See the INSTALL file in the mathcomp package for instructions on
upgrading projects from 1.5 to 1.6.  The 1.6 version works with both Coq
8.4 and 8.5.

4 files changed, 39 insertions, 34 deletions

diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 7c34e186717c..189b12206400 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -4,15 +4,15 @@ let src =
   if coq.coq-version == "8.4" then
 
     fetchurl {
-      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
-      sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
+      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
+      sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
     }
 
   else if coq.coq-version == "8.5" then
 
     fetchurl {
-      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;
-      sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";
+      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
+      sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
     }
 
   else throw "No mathcomp package for Coq version ${coq.coq-version}";
diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix
index 56838734b6d3..b4048aa80037 100644
--- a/pkgs/development/coq-modules/mathcomp/generic.nix
+++ b/pkgs/development/coq-modules/mathcomp/generic.nix
@@ -1,25 +1,33 @@
-{ stdenv, fetchurl, coq, ssreflect
-, graphviz, ocamlPackages, withDoc ? true
+{ stdenv, fetchurl, coq, ssreflect, ncurses, which
+, graphviz, ocamlPackages, withDoc ? false
 , src
 }:
 
 stdenv.mkDerivation {
 
-  name = "coq-mathcomp-1.5-${coq.coq-version}";
+  name = "coq-mathcomp-1.6-${coq.coq-version}";
 
   inherit src;
 
-  nativeBuildInputs = stdenv.lib.optionals withDoc
-    ([ graphviz ] ++ (with ocamlPackages; [ ocaml camlp5_transitional ]));
-  propagatedBuildInputs = [ ssreflect ];
+  nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
+  buildInputs = [ coq.ocaml coq.camlp5 ncurses which ];
+  propagatedBuildInputs = [ coq ssreflect ];
 
   enableParallelBuilding = true;
 
   buildFlags = stdenv.lib.optionalString withDoc "doc";
 
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+  preBuild = ''
+    cd mathcomp
+    export COQBIN=${coq}/bin/
+  '';
 
-  postInstall = stdenv.lib.optionalString withDoc ''
+  installPhase = ''
+    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
+    rm -fr $out/lib/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect*
+    rm -fr $out/lib/coq/${coq.coq-version}/user-contrib/ssrmatching.cmi
+    rm -fr $out/share/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect*
+  '' + stdenv.lib.optionalString withDoc ''
     make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
   '';
 
diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix
index a0b0d951c0df..8ba49d06bae9 100644
--- a/pkgs/development/coq-modules/ssreflect/default.nix
+++ b/pkgs/development/coq-modules/ssreflect/default.nix
@@ -5,8 +5,8 @@ if coq.coq-version == "8.4" then
 callPackage ./generic.nix {
 
   src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz;
-    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
+    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
+    sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
   };
 
 }
@@ -16,12 +16,10 @@ else if coq.coq-version == "8.5" then
 callPackage ./generic.nix {
 
   src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz;
-    sha256 = "084l9xd5vgb8jml0dkm66g8cil5rsf04w821pjhn2qk9mdbwaagf";
+    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
+    sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
   };
 
-  patches = [ ./threads.patch ];
-
 }
 
 else throw "No ssreflect package for Coq version ${coq.coq-version}"
diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix
index 3bfccab0be7d..d7303ad8852c 100644
--- a/pkgs/development/coq-modules/ssreflect/generic.nix
+++ b/pkgs/development/coq-modules/ssreflect/generic.nix
@@ -1,39 +1,38 @@
-{ stdenv, fetchurl, coq, ncurses
-, graphviz, withDoc ? true
+{ stdenv, fetchurl, coq, ncurses, which
+, graphviz, withDoc ? false
 , src, patches ? []
 }:
 
 stdenv.mkDerivation {
 
-  name = "coq-ssreflect-1.5-${coq.coq-version}";
+  name = "coq-ssreflect-1.6-${coq.coq-version}";
 
   inherit src;
 
   nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq.ocaml coq.camlp5 ncurses ];
+  buildInputs = [ coq.ocaml coq.camlp5 ncurses which ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;
 
   inherit patches;
 
-  postPatch = ''
-    # Permit building of the ssrcoq statically-bound executable
-    sed -i 's/^#-custom/-custom/' Make
-    sed -i 's/^#SSRCOQ/SSRCOQ/' Make
+  preBuild = ''
+    cd mathcomp/ssreflect
+    export COQBIN=${coq}/bin/
   '';
 
-  buildFlags = stdenv.lib.optionalString withDoc "doc";
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+  installPhase = ''
+    make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install
+  '';
 
   postInstall = ''
-    mkdir -p $out/bin
-    cp -p bin/ssrcoq $out/bin
-    cp -p bin/ssrcoq.byte $out/bin
+    # mkdir -p $out/bin
+    # cp -p bin/ssrcoq $out/bin
+    # cp -p bin/ssrcoq.byte $out/bin
   '' + stdenv.lib.optionalString withDoc ''
-    mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/
-    cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/Ssreflect/
+    mkdir -p $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/
+    cp -r html $out/share/doc/coq/${coq.coq-version}/user-contrib/mathcomp/ssreflect/
   '';
 
   meta = with stdenv.lib; {