From 01571ab2d796d136987c8759fe9b7347ea9a7720 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 28 May 2015 20:31:12 +0200
Subject: [PATCH] coq-mathcomp: refactor

---
 pkgs/development/coq-modules/mathcomp/1.5.nix | 26 -----------
 .../coq-modules/mathcomp/default.nix          | 43 +++++++------------
 .../coq-modules/mathcomp/generic.nix          | 33 ++++++++++++++
 pkgs/top-level/all-packages.nix               |  4 +-
 4 files changed, 52 insertions(+), 54 deletions(-)
 delete mode 100644 pkgs/development/coq-modules/mathcomp/1.5.nix
 create mode 100644 pkgs/development/coq-modules/mathcomp/generic.nix

diff --git a/pkgs/development/coq-modules/mathcomp/1.5.nix b/pkgs/development/coq-modules/mathcomp/1.5.nix
deleted file mode 100644
index c984bab4917..00000000000
--- a/pkgs/development/coq-modules/mathcomp/1.5.nix
+++ /dev/null
@@ -1,26 +0,0 @@
-{stdenv, fetchurl, coq, ssreflect}:
-
-stdenv.mkDerivation {
-
-  name = "coq-mathcomp-1.5-8.5b2";
-
-  src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;
-    sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";
-  };
-
-  propagatedBuildInputs = [ coq ssreflect ];
-
-  enableParallelBuilding = true;
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  meta = with stdenv.lib; {
-    homepage = http://ssr.msr-inria.inria.fr/;
-    license = licenses.cecill-b;
-    maintainers = [ maintainers.vbgl maintainers.jwiegley ];
-    platforms = coq.meta.platforms;
-    hydraPlatforms = [];
-  };
-
-}
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 9ebfba98d83..7c34e186717 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -1,35 +1,24 @@
-{ stdenv, fetchurl, coq, ssreflect
-, graphviz, ocaml, withDoc ? true
-}:
+{ callPackage, coq, fetchurl }:
 
-stdenv.mkDerivation {
+let src = 
+  if coq.coq-version == "8.4" then
 
-  name = "coq-mathcomp-1.5";
+    fetchurl {
+      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
+      sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
+    }
 
-  src = fetchurl {
-    url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.tar.gz;
-    sha256 = "1297svwi18blrlyd8vsqilar2h5nfixlvlifdkbx47aljq4m5bam";
-  };
+  else if coq.coq-version == "8.5" then
 
-  nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ocaml ];
-  propagatedBuildInputs = [ coq ssreflect ];
+    fetchurl {
+      url = http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz;
+      sha256 = "03bnq44ym43x8shi7whc02l0g5vy6rx8f1imjw478chlgwcxazqy";
+    }
 
-  enableParallelBuilding = true;
+  else throw "No mathcomp package for Coq version ${coq.coq-version}";
 
-  buildFlags = stdenv.lib.optionalString withDoc "doc";
-
-  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
-
-  postInstall = stdenv.lib.optionalString withDoc ''
-    make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
-  '';
-
-  meta = with stdenv.lib; {
-    homepage = http://ssr.msr-inria.inria.fr/;
-    license = licenses.cecill-b;
-    maintainers = [ maintainers.vbgl maintainers.jwiegley ];
-    platforms = coq.meta.platforms;
-    hydraPlatforms = [];
-  };
+in
 
+callPackage ./generic.nix {
+  inherit src;
 }
diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix
new file mode 100644
index 00000000000..3748152b68a
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp/generic.nix
@@ -0,0 +1,33 @@
+{ stdenv, fetchurl, coq, ssreflect
+, graphviz, ocamlPackages, withDoc ? true
+, src
+}:
+
+stdenv.mkDerivation {
+
+  name = "coq-${coq.coq-version}-mathcomp-1.5";
+
+  inherit src;
+
+  nativeBuildInputs = stdenv.lib.optionals withDoc
+    ([ graphviz ] ++ (with ocamlPackages; [ ocaml camlp5_transitional ]));
+  propagatedBuildInputs = [ ssreflect ];
+
+  enableParallelBuilding = true;
+
+  buildFlags = stdenv.lib.optionalString withDoc "doc";
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  postInstall = stdenv.lib.optionalString withDoc ''
+    make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/
+  '';
+
+  meta = with stdenv.lib; {
+    homepage = http://ssr.msr-inria.inria.fr/;
+    license = licenses.cecill-b;
+    maintainers = [ maintainers.vbgl maintainers.jwiegley ];
+    platforms = coq.meta.platforms;
+  };
+
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ef80fcd5e08..0959b25fad5 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -14048,6 +14048,8 @@ let
 
   mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
 
+    inherit callPackage;
+
     bedrock = callPackage ../development/coq-modules/bedrock {};
 
     contribs =
@@ -14094,7 +14096,7 @@ let
 
     coq = coq_8_5;
 
-    mathcomp = callPackage ../development/coq-modules/mathcomp/1.5.nix { };
+    mathcomp = callPackage ../development/coq-modules/mathcomp { };
 
     ssreflect = callPackage ../development/coq-modules/ssreflect { };