coqPackages: move to a separate file and filter the package set

9 files changed, 115 insertions, 70 deletions

diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
index ec190d5a1d6..3f5ec69235f 100644
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -1,8 +1,4 @@
-{ stdenv, fetchurl, coq, coqPackages }:
-
-if !stdenv.lib.versionAtLeast coq.coq-version "8.6"
-then throw "CoLoR is not available for Coq ${coq.coq-version}"
-else
+{ stdenv, fetchurl, coq, bignums }:
 
 stdenv.mkDerivation {
   name = "coq${coq.coq-version}-CoLoR-1.4.0";
@@ -12,7 +8,7 @@ stdenv.mkDerivation {
     sha256 = "1jsp9adsh7w59y41ihbwchryjhjpajgs9bhf8rnb4b3hzccqxgag";
   };
 
-  buildInputs = [ coq coqPackages.bignums ];
+  buildInputs = [ coq bignums ];
   enableParallelBuilding = false;
 
   installPhase = ''
@@ -25,4 +21,8 @@ stdenv.mkDerivation {
     maintainers = with maintainers; [ jwiegley ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
+  };
 }
diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix
index cb77ac3deac..fb01da8d59c 100644
--- a/pkgs/development/coq-modules/HoTT/default.nix
+++ b/pkgs/development/coq-modules/HoTT/default.nix
@@ -1,8 +1,6 @@
 { stdenv, fetchFromGitHub, autoconf, automake, coq }:
 
-if !stdenv.lib.versionAtLeast coq.coq-version "8.6"
-then throw "This version of HoTT requires Coq 8.6"
-else stdenv.mkDerivation rec {
+stdenv.mkDerivation rec {
   name = "coq${coq.coq-version}-HoTT-${version}";
   version = "20170921";
 
@@ -56,4 +54,8 @@ else stdenv.mkDerivation rec {
     maintainers = with maintainers; [ siddharthist ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = {
+    compatibleCoqVersions = v: v == "8.6";
+  };
 }
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
index 143e0344cf3..766a10c9579 100644
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@@ -42,4 +42,8 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
+  };
+
 }
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index eb05a1be53e..34210ba01bb 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -42,4 +42,8 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
+  };
+
 }
diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix
index dc411763da5..b970747c772 100644
--- a/pkgs/development/coq-modules/fiat/HEAD.nix
+++ b/pkgs/development/coq-modules/fiat/HEAD.nix
@@ -30,7 +30,9 @@ stdenv.mkDerivation rec {
     description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
     maintainers = with maintainers; [ jwiegley ];
     platforms = coq.meta.platforms;
-    broken = stdenv.lib.versionAtLeast coq.coq-version "8.6";
   };
 
+  passthru = {
+    compatibleCoqVersions = v: v == "8.5";
+  };
 }
diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix
index d045ec4223b..1831cd0c571 100644
--- a/pkgs/development/coq-modules/math-classes/default.nix
+++ b/pkgs/development/coq-modules/math-classes/default.nix
@@ -1,8 +1,4 @@
-{ stdenv, fetchFromGitHub, coq, coqPackages }:
-
-if ! stdenv.lib.versionAtLeast coq.coq-version "8.6" then
-  throw "Math-Classes requires Coq 8.6 or later."
-else
+{ stdenv, fetchFromGitHub, coq, bignums }:
 
 stdenv.mkDerivation rec {
 
@@ -16,7 +12,7 @@ stdenv.mkDerivation rec {
     sha256 = "0wgnczacvkb2pc3vjbni9bwjijfyd5jcdnyyjg8185hkf9zzabgi";
   };
 
-  buildInputs = [ coq coqPackages.bignums ];
+  buildInputs = [ coq bignums ];
   enableParallelBuilding = true;
   installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 
@@ -26,4 +22,9 @@ stdenv.mkDerivation rec {
     maintainers = with maintainers; [ siddharthist jwiegley ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
+  };
+
 }
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix
index 0304cb48b3b..f6316f77a1f 100644
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchgit, coq, ocamlPackages, haskellPackages, which, ott
+{ stdenv, fetchgit, coq, haskellPackages, which, ott
 }:
 
 stdenv.mkDerivation rec {
@@ -29,8 +29,7 @@ stdenv.mkDerivation rec {
     license = stdenv.lib.licenses.mit;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott ]
-    ++ (with ocamlPackages; [ findlib ]);
+  buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott coq.findlib ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;
@@ -50,4 +49,8 @@ stdenv.mkDerivation rec {
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
+  };
+
 }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 53f0234d604..dc5b26069f6 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -18825,57 +18825,12 @@ with pkgs;
 
   boogie = dotnetPackages.Boogie;
 
-  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
-    make = pkgs.gnumake3;
-    inherit (ocamlPackages_3_12_1) ocaml findlib;
-    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
-    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
-  };
-  coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
-    inherit (ocamlPackages_4_02) ocaml findlib lablgtk;
-    camlp5 = ocamlPackages_4_02.camlp5_transitional;
-  };
-  coq_8_5 = callPackage ../applications/science/logic/coq {
-    version = "8.5pl3";
-  };
-  coq_8_6 = callPackage ../applications/science/logic/coq {};
-  coq_8_7 = callPackage ../applications/science/logic/coq {
-    version = "8.7.1";
-  };
-
-  mkCoqPackages = self: coq: let callPackage = newScope self; in rec {
-    inherit callPackage coq;
-    coqPackages = self;
-
-    autosubst = callPackage ../development/coq-modules/autosubst {};
-    bignums = if stdenv.lib.versionAtLeast coq.coq-version "8.6"
-      then callPackage ../development/coq-modules/bignums {}
-      else null;
-    coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
-    coquelicot = callPackage ../development/coq-modules/coquelicot {};
-    dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
-    flocq = callPackage ../development/coq-modules/flocq {};
-    heq = callPackage ../development/coq-modules/heq {};
-    HoTT = callPackage ../development/coq-modules/HoTT {};
-    interval = callPackage ../development/coq-modules/interval {};
-    mathcomp = callPackage ../development/coq-modules/mathcomp { };
-    metalib = callPackage ../development/coq-modules/metalib { };
-    paco = callPackage ../development/coq-modules/paco {};
-    ssreflect = callPackage ../development/coq-modules/ssreflect { };
-    QuickChick = callPackage ../development/coq-modules/QuickChick {};
-    CoLoR = callPackage ../development/coq-modules/CoLoR {};
-    math-classes = callPackage ../development/coq-modules/math-classes { };
-    fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
-    equations = callPackage ../development/coq-modules/equations { };
-    coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
-    category-theory = callPackage ../development/coq-modules/category-theory { };
-  };
-
-  coqPackages_8_5 = mkCoqPackages coqPackages_8_5 coq_8_5;
-  coqPackages_8_6 = mkCoqPackages coqPackages_8_6 coq_8_6;
-  coqPackages_8_7 = mkCoqPackages coqPackages_8_7 coq_8_7;
-  coqPackages = coqPackages_8_6;
-  coq = coqPackages.coq;
+  inherit (callPackage ./coq-packages.nix {})
+    mkCoqPackages
+    coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7
+    coqPackages_8_5 coqPackages_8_6 coqPackages_8_7
+    coqPackages coq
+  ;
 
   coq2html = callPackage ../applications/science/logic/coq2html {
     make = pkgs.gnumake3;
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
new file mode 100644
index 00000000000..34d9f09ff14
--- /dev/null
+++ b/pkgs/top-level/coq-packages.nix
@@ -0,0 +1,74 @@
+{ lib, callPackage, newScope
+, gnumake3
+, ocamlPackages_3_12_1
+, ocamlPackages_4_02
+}:
+
+let
+  mkCoqPackages' = self: coq:
+    let callPackage = newScope self ; in rec {
+      inherit callPackage coq;
+      coqPackages = self;
+
+      autosubst = callPackage ../development/coq-modules/autosubst {};
+      bignums = if lib.versionAtLeast coq.coq-version "8.6"
+        then callPackage ../development/coq-modules/bignums {}
+        else null;
+      category-theory = callPackage ../development/coq-modules/category-theory { };
+      CoLoR = callPackage ../development/coq-modules/CoLoR {};
+      coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
+      coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
+      coquelicot = callPackage ../development/coq-modules/coquelicot {};
+      dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
+      equations = callPackage ../development/coq-modules/equations { };
+      fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
+      flocq = callPackage ../development/coq-modules/flocq {};
+      heq = callPackage ../development/coq-modules/heq {};
+      HoTT = callPackage ../development/coq-modules/HoTT {};
+      interval = callPackage ../development/coq-modules/interval {};
+      math-classes = callPackage ../development/coq-modules/math-classes { };
+      mathcomp = callPackage ../development/coq-modules/mathcomp { };
+      metalib = callPackage ../development/coq-modules/metalib { };
+      paco = callPackage ../development/coq-modules/paco {};
+      QuickChick = callPackage ../development/coq-modules/QuickChick {};
+      ssreflect = callPackage ../development/coq-modules/ssreflect { };
+    };
+
+  filterCoqPackages = coq:
+    lib.filterAttrs
+    (_: p:
+      let pred = p.compatibleCoqVersions or (_: true);
+      in pred coq.coq-version
+    );
+
+in rec {
+
+  mkCoqPackages = coq:
+    let self = mkCoqPackages' self coq; in
+    filterCoqPackages coq self;
+
+  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
+    make = gnumake3;
+    inherit (ocamlPackages_3_12_1) ocaml findlib;
+    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
+    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
+  };
+  coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
+    inherit (ocamlPackages_4_02) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages_4_02.camlp5_transitional;
+  };
+  coq_8_5 = callPackage ../applications/science/logic/coq {
+    version = "8.5pl3";
+  };
+  coq_8_6 = callPackage ../applications/science/logic/coq {};
+  coq_8_7 = callPackage ../applications/science/logic/coq {
+    version = "8.7.1";
+  };
+
+  coqPackages_8_5 = mkCoqPackages coq_8_5;
+  coqPackages_8_6 = mkCoqPackages coq_8_6;
+  coqPackages_8_7 = mkCoqPackages coq_8_7;
+  coqPackages = coqPackages_8_6;
+  coq = coqPackages.coq;
+
+}