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.

2 files changed, 19 insertions, 22 deletions

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; {