Merge pull request #32737 from vbgl/coq-packages-filter

Tidy up the Coq package sets

doc/languages-frameworks/coq.xml

@@ -11,31 +11,53 @@
     in the Coq derivation.
   </para>
   <para>
-    Some libraries require OCaml and sometimes also Camlp5. The exact
+    Some libraries require OCaml and sometimes also Camlp5 or findlib.
-    versions that were used to build Coq are saved in the
+    The exact versions that were used to build Coq are saved in the
     <literal>coq.ocaml</literal> and <literal>coq.camlp5</literal>
-    attributes.
+    and <literal>coq.findlib</literal> attributes.
+  </para>
+  <para>
+    Coq libraries may be compatible with some specific versions of Coq only.
+    The <liberal>compatibleCoqVersions</liberal> attribute is used to
+    precisely select those versions of Coq that are compatible with this
+    derivation.
   </para>
   <para>
     Here is a simple package example. It is a pure Coq library, thus it
-    only depends on Coq. Its <literal>makefile</literal> has been
+    depends on Coq. It builds on the Mathematical Components library, thus it
-    generated using <literal>coq_makefile</literal> so we only have to
+    also takes <literal>mathcomp</literal> as <literal>buildInputs</literal>.
+    Its <literal>Makefile</literal> has been generated using
+    <literal>coq_makefile</literal> so we only have to
     set the <literal>$COQLIB</literal> variable at install time.
   </para>
   <programlisting>
-{stdenv, fetchurl, coq}:
+{ stdenv, fetchFromGitHub, coq, mathcomp }:
-stdenv.mkDerivation {
+
-  src = fetchurl {
+stdenv.mkDerivation rec {
-    url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz;
+  name = "coq${coq.coq-version}-multinomials-${version}";
-    sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1";
+  version = "1.0";
+  src = fetchFromGitHub {
+    owner = "math-comp";
+    repo = "multinomials";
+    rev = version;
+    sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
   };
 
-  name = "coq-karatsuba";
-
   buildInputs = [ coq ];
+  propagatedBuildInputs = [ mathcomp ];
 
   installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    inherit (src.meta) homepage;
+    license = stdenv.lib.licenses.cecill-b;
+    inherit (coq.meta) platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
 }
 </programlisting>
 </section>
-

pkgs/applications/science/logic/coq/default.nix

@@ -9,7 +9,7 @@
 , ocamlPackages, ncurses
 , buildIde ? true
 , csdp ? null
-, version ? "8.6.1"
+, version ? "8.7.1"
 }:
 
 let
@@ -19,7 +19,6 @@ let
    "8.5pl3"    = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw";
    "8.6"       = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4";
    "8.6.1"     = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l";
-   "8.7+beta2" = "1r274m44z774xigvj43g211ms9z9bwgyp1g43rvq4fswb3gzxc4b";
    "8.7.0"     = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
    "8.7.1"     = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
   }."${version}";

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

@@ -1,8 +1,4 @@
-{ stdenv, fetchurl, coq, coqPackages }:
+{ stdenv, fetchurl, coq, bignums }:
-
-if !stdenv.lib.versionAtLeast coq.coq-version "8.6"
-then throw "CoLoR is not available for Coq ${coq.coq-version}"
-else
 
 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";
+  };
 }

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"
+stdenv.mkDerivation rec {
-then throw "This version of HoTT requires Coq 8.6"
-else 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";
+  };
 }

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

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

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

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

@@ -1,8 +1,4 @@
-{ stdenv, fetchFromGitHub, coq, coqPackages }:
+{ stdenv, fetchFromGitHub, coq, bignums }:
-
-if ! stdenv.lib.versionAtLeast coq.coq-version "8.6" then
-  throw "Math-Classes requires Coq 8.6 or later."
-else
 
 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";
+  };
+
 }

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 ]
+  buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott coq.findlib ];
-    ++ (with ocamlPackages; [ 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";
+  };
+
 }

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

@@ -0,0 +1,28 @@
+{ stdenv, fetchFromGitHub, coq, mathcomp }:
+
+stdenv.mkDerivation rec {
+  name = "coq${coq.coq-version}-multinomials-${version}";
+  version = "1.0";
+  src = fetchFromGitHub {
+    owner = "math-comp";
+    repo = "multinomials";
+    rev = version;
+    sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
+  };
+
+  buildInputs = [ coq ];
+  propagatedBuildInputs = [ mathcomp ];
+
+  installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
+
+  meta = {
+    description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
+    inherit (src.meta) homepage;
+    license = stdenv.lib.licenses.cecill-b;
+    inherit (coq.meta) platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ];
+  };
+}

pkgs/top-level/all-packages.nix

@@ -18831,57 +18831,12 @@ with pkgs;
 
   boogie = dotnetPackages.Boogie;
 
-  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
+  inherit (callPackage ./coq-packages.nix {})
-    make = pkgs.gnumake3;
+    mkCoqPackages
-    inherit (ocamlPackages_3_12_1) ocaml findlib;
+    coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7
-    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
+    coqPackages_8_5 coqPackages_8_6 coqPackages_8_7
-    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
+    coqPackages coq
-  };
+  ;
-  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;
 
   coq2html = callPackage ../applications/science/logic/coq2html {
     make = pkgs.gnumake3;

pkgs/top-level/coq-packages.nix

@@ -0,0 +1,75 @@
+{ 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 { };
+      multinomials = callPackage ../development/coq-modules/multinomials {};
+      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 {
+    version = "8.6.1";
+  };
+  coq_8_7 = callPackage ../applications/science/logic/coq {};
+
+  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;
+
+}