2017-12-22 16:56:20 +00:00
|
|
|
{ lib, callPackage, newScope, recurseIntoAttrs
|
2017-12-15 19:52:16 +00:00
|
|
|
, gnumake3
|
|
|
|
, ocamlPackages_3_12_1
|
|
|
|
, ocamlPackages_4_02
|
2018-08-21 21:22:24 +00:00
|
|
|
, ocamlPackages_4_05
|
2017-12-15 19:52:16 +00:00
|
|
|
}:
|
|
|
|
|
|
|
|
let
|
|
|
|
mkCoqPackages' = self: coq:
|
|
|
|
let callPackage = newScope self ; in rec {
|
|
|
|
inherit callPackage coq;
|
|
|
|
coqPackages = self;
|
|
|
|
|
2017-12-22 16:56:20 +00:00
|
|
|
contribs = recurseIntoAttrs
|
|
|
|
(callPackage ../development/coq-modules/contribs {});
|
|
|
|
|
2017-12-15 19:52:16 +00:00
|
|
|
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 {};
|
2018-05-22 17:26:32 +00:00
|
|
|
iris = callPackage ../development/coq-modules/iris {};
|
2017-12-15 19:52:16 +00:00
|
|
|
math-classes = callPackage ../development/coq-modules/math-classes { };
|
|
|
|
mathcomp = callPackage ../development/coq-modules/mathcomp { };
|
|
|
|
metalib = callPackage ../development/coq-modules/metalib { };
|
2017-12-18 01:28:57 +00:00
|
|
|
multinomials = callPackage ../development/coq-modules/multinomials {};
|
2017-12-15 19:52:16 +00:00
|
|
|
paco = callPackage ../development/coq-modules/paco {};
|
|
|
|
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
|
|
|
ssreflect = callPackage ../development/coq-modules/ssreflect { };
|
2018-05-15 20:48:20 +00:00
|
|
|
stdpp = callPackage ../development/coq-modules/stdpp { };
|
2017-12-19 14:26:11 +00:00
|
|
|
tlc = callPackage ../development/coq-modules/tlc {};
|
2017-12-15 19:52:16 +00:00
|
|
|
};
|
|
|
|
|
|
|
|
filterCoqPackages = coq:
|
2017-12-22 16:56:20 +00:00
|
|
|
lib.filterAttrsRecursive
|
2017-12-15 19:52:16 +00:00
|
|
|
(_: 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 {
|
2018-08-21 21:22:24 +00:00
|
|
|
ocamlPackages = ocamlPackages_4_05;
|
2017-12-15 19:52:16 +00:00
|
|
|
version = "8.5pl3";
|
|
|
|
};
|
2017-12-16 06:14:41 +00:00
|
|
|
coq_8_6 = callPackage ../applications/science/logic/coq {
|
|
|
|
version = "8.6.1";
|
2017-12-15 19:52:16 +00:00
|
|
|
};
|
2017-12-21 09:24:35 +00:00
|
|
|
coq_8_7 = callPackage ../applications/science/logic/coq {
|
2018-02-16 07:12:01 +00:00
|
|
|
version = "8.7.2";
|
2017-12-21 09:24:35 +00:00
|
|
|
};
|
2018-03-21 14:00:47 +00:00
|
|
|
coq_8_8 = callPackage ../applications/science/logic/coq {
|
2018-06-29 09:10:31 +00:00
|
|
|
version = "8.8.1";
|
2018-03-21 14:00:47 +00:00
|
|
|
};
|
2017-12-15 19:52:16 +00:00
|
|
|
|
|
|
|
coqPackages_8_5 = mkCoqPackages coq_8_5;
|
|
|
|
coqPackages_8_6 = mkCoqPackages coq_8_6;
|
|
|
|
coqPackages_8_7 = mkCoqPackages coq_8_7;
|
2018-03-21 14:00:47 +00:00
|
|
|
coqPackages_8_8 = mkCoqPackages coq_8_8;
|
2018-08-07 12:58:23 +00:00
|
|
|
coqPackages = coqPackages_8_8;
|
2017-12-15 19:52:16 +00:00
|
|
|
coq = coqPackages.coq;
|
|
|
|
|
|
|
|
}
|