diff --git a/doc/languages-frameworks/coq.xml b/doc/languages-frameworks/coq.xml index d16c9f3dc87..43da6a3f49d 100644 --- a/doc/languages-frameworks/coq.xml +++ b/doc/languages-frameworks/coq.xml @@ -11,31 +11,53 @@ in the Coq derivation. - Some libraries require OCaml and sometimes also Camlp5. The exact - versions that were used to build Coq are saved in the + Some libraries require OCaml and sometimes also Camlp5 or findlib. + The exact versions that were used to build Coq are saved in the coq.ocaml and coq.camlp5 - attributes. + and coq.findlib attributes. + + + Coq libraries may be compatible with some specific versions of Coq only. + The compatibleCoqVersions attribute is used to + precisely select those versions of Coq that are compatible with this + derivation. Here is a simple package example. It is a pure Coq library, thus it - only depends on Coq. Its makefile has been - generated using coq_makefile so we only have to + depends on Coq. It builds on the Mathematical Components library, thus it + also takes mathcomp as buildInputs. + Its Makefile has been generated using + coq_makefile so we only have to set the $COQLIB variable at install time. -{stdenv, fetchurl, coq}: -stdenv.mkDerivation { - src = fetchurl { - url = http://coq.inria.fr/pylons/contribs/files/Karatsuba/v8.4/Karatsuba.tar.gz; - sha256 = "0ymfpv4v49k4fm63nq6gcl1hbnnxrvjjp7yzc4973n49b853c5b1"; +{ 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"; }; - 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" ]; + }; } - diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 2aa40b391f7..6ab98f30ae6 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/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}"; 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/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix new file mode 100644 index 00000000000..aa22c96256f --- /dev/null +++ b/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" ]; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index b24d48f0d12..1a8e2d38822 100644 --- a/pkgs/top-level/all-packages.nix +++ b/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 { - 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..076347e3b66 --- /dev/null +++ b/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; + +}