diff options
Diffstat (limited to 'pkgs/top-level/coq-packages.nix')
-rw-r--r-- | pkgs/top-level/coq-packages.nix | 74 |
1 files changed, 74 insertions, 0 deletions
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; + +} |