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

pkgs/development/coq-modules/CoLoR/default.nix

···
-{ 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";
···
     sha256 = "1jsp9adsh7w59y41ihbwchryjhjpajgs9bhf8rnb4b3hzccqxgag";
   };
 
-  buildInputs = [ coq coqPackages.bignums ];
+  buildInputs = [ coq bignums ];
   enableParallelBuilding = false;
 
   installPhase = ''
···
     description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";
     maintainers = with maintainers; [ jwiegley ];
     platforms = coq.meta.platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
   };
 }

pkgs/development/coq-modules/HoTT/default.nix

···
 { 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";
 
···
     description = "Homotopy type theory";
     maintainers = with maintainers; [ siddharthist ];
     platforms = coq.meta.platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: v == "8.6";
   };
 }

pkgs/development/coq-modules/category-theory/default.nix

···
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
+  };
+
 }

pkgs/development/coq-modules/equations/default.nix

···
     platforms = coq.meta.platforms;
   };
 
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ];
+  };
+
 }

pkgs/development/coq-modules/fiat/HEAD.nix

···
     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";
+  };
 }

pkgs/development/coq-modules/math-classes/default.nix

···
-{ 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 {
 
···
     sha256 = "0wgnczacvkb2pc3vjbni9bwjijfyd5jcdnyyjg8185hkf9zzabgi";
   };
 
-  buildInputs = [ coq coqPackages.bignums ];
+  buildInputs = [ coq bignums ];
   enableParallelBuilding = true;
   installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 
···
     maintainers = with maintainers; [ siddharthist jwiegley ];
     platforms = coq.meta.platforms;
   };
+
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
+  };
+
 }

pkgs/development/coq-modules/metalib/default.nix

···
-{ stdenv, fetchgit, coq, ocamlPackages, haskellPackages, which, ott
+{ stdenv, fetchgit, coq, haskellPackages, which, ott
 }:
 
 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;
···
     license = licenses.mit;
     maintainers = [ maintainers.jwiegley ];
     platforms = coq.meta.platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.6";
   };
 
 }

pkgs/top-level/all-packages.nix

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

pkgs/top-level/coq-packages.nix

···
+{ 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;
+
+}