coqPackages.{ssreflect,mathcomp}: fix build with Coq-8.6

by adding `findlib` as a build input. Also clean `default.nix` a little bit.
NixOS · Jan 25, 2017 · 42bf99e · 42bf99e
1 parent 635ac15
commit 42bf99e
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 65 deletions.
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -1,39 +1,22 @@
 { callPackage, fetchurl, coq }:
 
-if coq.coq-version == "8.4" then
-
-callPackage ./generic.nix {
-
-  name = "coq-mathcomp-1.6-${coq.coq-version}";
-  src = fetchurl {
+let param =
+  let v16 = {
+    version = "1.6";
     url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
     sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
-  };
-
-}
-
-else if coq.coq-version == "8.5" then
-
-callPackage ./generic.nix {
-
-  name = "coq-mathcomp-1.6-${coq.coq-version}";
-  src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
-    sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
-  };
-
-}
-
-else if coq.coq-version == "8.6" then
-
-callPackage ./generic.nix {
-
-  name = "coq-mathcomp-1.6.1-${coq.coq-version}";
-  src = fetchurl {
+  }; v161 = {
+    version = "1.6.1";
     url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
     sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
-  };
+  }; in
+{
+  "8.4" = v16;
+  "8.5" = v16;
+  "8.6" = v161;
+}."${coq.coq-version}"; in
 
+callPackage ./generic.nix {
+  name = "coq${coq.coq-version}-mathcomp-${param.version}";
+  src = fetchurl { inherit (param) url sha256; };
 }
-
-else throw "No ssreflect 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
@@ -1,5 +1,5 @@
 { stdenv, fetchurl, coq, ssreflect, ncurses, which
-, graphviz, ocamlPackages, withDoc ? false
+, graphviz, withDoc ? false
 , src, name
 }:
 
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
   inherit src;
 
   nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq.ocaml coq.camlp5 ncurses which ];
+  buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ];
   propagatedBuildInputs = [ coq ssreflect ];
 
   enableParallelBuilding = true;

diff --git a/pkgs/development/coq-modules/ssreflect/default.nix b/pkgs/development/coq-modules/ssreflect/default.nix
@@ -1,39 +1,22 @@
 { callPackage, fetchurl, coq }:
 
-if coq.coq-version == "8.4" then
-
-callPackage ./generic.nix {
-
-  name = "coq-ssreflect-1.6-${coq.coq-version}";
-  src = fetchurl {
+let param =
+  let v16 = {
+    version = "1.6";
     url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
     sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
-  };
-
-}
-
-else if coq.coq-version == "8.5" then
-
-callPackage ./generic.nix {
-
-  name = "coq-ssreflect-1.6-${coq.coq-version}";
-  src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.6.tar.gz;
-    sha256 = "0adr556032r1jkvphbpfvrrv041qk0yqb7a1xnbam52ji0mdl2w8";
-  };
-
-}
-
-else if coq.coq-version == "8.6" then
-
-callPackage ./generic.nix {
-
-  name = "coq-ssreflect-1.6.1-${coq.coq-version}";
-  src = fetchurl {
+  }; v161 = {
+    version = "1.6.1";
     url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
     sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
-  };
+  }; in
+{
+  "8.4" = v16;
+  "8.5" = v16;
+  "8.6" = v161;
+}."${coq.coq-version}"; in
 
+callPackage ./generic.nix {
+  name = "coq${coq.coq-version}-ssreflect-${param.version}";
+  src = fetchurl { inherit (param) url sha256; };
 }
-
-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
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
   inherit src;
 
   nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq.ocaml coq.camlp5 ncurses which ];
+  buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;