2020-12-07 21:03:47 +00:00
|
|
|
{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
|
|
|
|
, compcert
|
|
|
|
}:
|
2017-12-15 19:52:16 +00:00
|
|
|
|
|
|
|
let
|
|
|
|
mkCoqPackages' = self: coq:
|
2019-06-16 20:59:06 +01:00
|
|
|
let callPackage = self.callPackage; in {
|
2019-04-09 00:07:42 +01:00
|
|
|
inherit coq;
|
2017-12-15 19:52:16 +00:00
|
|
|
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 { };
|
2018-11-20 23:16:27 +00:00
|
|
|
Cheerios = callPackage ../development/coq-modules/Cheerios {};
|
2017-12-15 19:52:16 +00:00
|
|
|
CoLoR = callPackage ../development/coq-modules/CoLoR {};
|
2019-10-22 19:19:45 +01:00
|
|
|
coq-bits = callPackage ../development/coq-modules/coq-bits {};
|
2019-08-06 10:15:37 +01:00
|
|
|
coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
|
2017-12-15 19:52:16 +00:00
|
|
|
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
|
|
|
|
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
|
2019-03-22 09:10:55 +00:00
|
|
|
coqhammer = callPackage ../development/coq-modules/coqhammer {};
|
2018-10-01 10:49:11 +01:00
|
|
|
coqprime = callPackage ../development/coq-modules/coqprime {};
|
2017-12-15 19:52:16 +00:00
|
|
|
coquelicot = callPackage ../development/coq-modules/coquelicot {};
|
2018-11-29 16:54:24 +00:00
|
|
|
corn = callPackage ../development/coq-modules/corn {};
|
2017-12-15 19:52:16 +00:00
|
|
|
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 {};
|
2019-06-13 16:25:38 +01:00
|
|
|
gappalib = callPackage ../development/coq-modules/gappalib {};
|
2017-12-15 19:52:16 +00:00
|
|
|
heq = callPackage ../development/coq-modules/heq {};
|
2020-03-10 14:21:07 +00:00
|
|
|
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
|
2017-12-15 19:52:16 +00:00
|
|
|
HoTT = callPackage ../development/coq-modules/HoTT {};
|
|
|
|
interval = callPackage ../development/coq-modules/interval {};
|
2018-11-20 23:16:27 +00:00
|
|
|
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
|
2018-05-22 18:26:32 +01:00
|
|
|
iris = callPackage ../development/coq-modules/iris {};
|
2019-05-22 10:42:06 +01:00
|
|
|
ltac2 = callPackage ../development/coq-modules/ltac2 {};
|
2017-12-15 19:52:16 +00:00
|
|
|
math-classes = callPackage ../development/coq-modules/math-classes { };
|
2020-03-10 14:21:07 +00:00
|
|
|
inherit (callPackage ../development/coq-modules/mathcomp {})
|
2020-05-09 06:47:47 +01:00
|
|
|
mathcomp_ mathcomp-config
|
|
|
|
mathcomp ssreflect
|
2019-05-23 14:45:28 +01:00
|
|
|
mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra
|
|
|
|
mathcomp-solvable mathcomp-field mathcomp-character
|
2020-05-09 06:47:47 +01:00
|
|
|
;
|
2019-04-09 18:21:57 +01:00
|
|
|
inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
|
2020-05-09 06:47:47 +01:00
|
|
|
mathcomp-extra-override mathcomp-extra-config mathcomp-extra
|
|
|
|
current-mathcomp-extra mathcomp-extra-fast mathcomp-extra-all
|
|
|
|
mathcomp-finmap mathcomp-bigenough mathcomp-real-closed
|
|
|
|
mathcomp-analysis multinomials coqeal
|
|
|
|
;
|
2017-12-15 19:52:16 +00:00
|
|
|
metalib = callPackage ../development/coq-modules/metalib { };
|
|
|
|
paco = callPackage ../development/coq-modules/paco {};
|
2019-02-11 09:04:26 +00:00
|
|
|
paramcoq = callPackage ../development/coq-modules/paramcoq {};
|
2017-12-15 19:52:16 +00:00
|
|
|
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
2018-12-03 14:45:03 +00:00
|
|
|
simple-io = callPackage ../development/coq-modules/simple-io { };
|
2018-05-15 21:48:20 +01:00
|
|
|
stdpp = callPackage ../development/coq-modules/stdpp { };
|
2018-11-20 23:16:27 +00:00
|
|
|
StructTact = callPackage ../development/coq-modules/StructTact {};
|
2017-12-19 14:26:11 +00:00
|
|
|
tlc = callPackage ../development/coq-modules/tlc {};
|
2018-10-24 01:08:56 +01:00
|
|
|
Velisarios = callPackage ../development/coq-modules/Velisarios {};
|
2018-11-20 23:16:27 +00:00
|
|
|
Verdi = callPackage ../development/coq-modules/Verdi {};
|
2020-12-07 21:03:47 +00:00
|
|
|
VST = callPackage ../development/coq-modules/VST {
|
|
|
|
compcert = compcert.override { version = "3.7"; };
|
|
|
|
};
|
2020-05-09 06:47:47 +01:00
|
|
|
|
|
|
|
filterPackages = filterCoqPackages;
|
2017-12-15 19:52:16 +00:00
|
|
|
};
|
|
|
|
|
2018-12-01 18:15:42 +00:00
|
|
|
filterCoqPackages = coq: set:
|
|
|
|
lib.listToAttrs (
|
|
|
|
lib.concatMap (name:
|
|
|
|
let v = set.${name}; in
|
|
|
|
let p = v.compatibleCoqVersions or (_: true); in
|
|
|
|
lib.optional (p coq.coq-version)
|
|
|
|
(lib.nameValuePair name (
|
|
|
|
if lib.isAttrs v && v.recurseForDerivations or false
|
|
|
|
then filterCoqPackages coq v
|
|
|
|
else v))
|
|
|
|
) (lib.attrNames set)
|
2017-12-15 19:52:16 +00:00
|
|
|
);
|
|
|
|
|
|
|
|
in rec {
|
|
|
|
|
2018-11-04 17:39:09 +00:00
|
|
|
/* The function `mkCoqPackages` takes as input a derivation for Coq and produces
|
|
|
|
* a set of libraries built with that specific Coq. More libraries are known to
|
|
|
|
* this function than what is compatible with that version of Coq. Therefore,
|
|
|
|
* libraries that are not known to be compatible are removed (filtered out) from
|
|
|
|
* the resulting set. For meta-programming purposes (inpecting the derivations
|
|
|
|
* rather than building the libraries) this filtering can be disabled by setting
|
|
|
|
* a `dontFilter` attribute into the Coq derivation.
|
|
|
|
*/
|
2017-12-15 19:52:16 +00:00
|
|
|
mkCoqPackages = coq:
|
2019-04-09 00:07:42 +01:00
|
|
|
let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in
|
2020-05-09 06:47:47 +01:00
|
|
|
if coq.dontFilter or false then self else filterCoqPackages coq self;
|
2017-12-15 19:52:16 +00:00
|
|
|
|
|
|
|
coq_8_5 = callPackage ../applications/science/logic/coq {
|
2018-08-21 22:22:24 +01: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 {
|
2018-08-21 22:33:13 +01:00
|
|
|
ocamlPackages = ocamlPackages_4_05;
|
2017-12-16 06:14:41 +00:00
|
|
|
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 {
|
2020-05-22 10:10:17 +01:00
|
|
|
ocamlPackages = ocamlPackages_4_09;
|
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 {
|
2020-05-22 10:10:17 +01:00
|
|
|
ocamlPackages = ocamlPackages_4_09;
|
2018-09-26 21:26:39 +01:00
|
|
|
version = "8.8.2";
|
2018-03-21 14:00:47 +00:00
|
|
|
};
|
2018-11-02 09:09:15 +00:00
|
|
|
coq_8_9 = callPackage ../applications/science/logic/coq {
|
2020-05-22 10:10:17 +01:00
|
|
|
ocamlPackages = ocamlPackages_4_09;
|
2019-05-22 10:04:19 +01:00
|
|
|
version = "8.9.1";
|
2018-11-02 09:09:15 +00:00
|
|
|
};
|
2019-05-14 09:31:49 +01:00
|
|
|
coq_8_10 = callPackage ../applications/science/logic/coq {
|
2020-05-22 10:10:17 +01:00
|
|
|
ocamlPackages = ocamlPackages_4_09;
|
2019-11-28 23:08:51 +00:00
|
|
|
version = "8.10.2";
|
2019-05-14 09:31:49 +01:00
|
|
|
};
|
2019-12-07 07:57:20 +00:00
|
|
|
coq_8_11 = callPackage ../applications/science/logic/coq {
|
2020-05-15 10:43:29 +01:00
|
|
|
version = "8.11.2";
|
2019-12-07 07:57:20 +00:00
|
|
|
};
|
2020-06-13 09:16:00 +01:00
|
|
|
coq_8_12 = callPackage ../applications/science/logic/coq {
|
2020-12-15 20:14:53 +00:00
|
|
|
version = "8.12.2";
|
2020-06-13 09:16:00 +01:00
|
|
|
};
|
2020-12-09 07:32:51 +00:00
|
|
|
coq_8_13 = callPackage ../applications/science/logic/coq {
|
|
|
|
version = "8.13+beta1";
|
|
|
|
};
|
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-11-02 09:09:15 +00:00
|
|
|
coqPackages_8_9 = mkCoqPackages coq_8_9;
|
2019-05-14 09:31:49 +01:00
|
|
|
coqPackages_8_10 = mkCoqPackages coq_8_10;
|
2019-12-07 07:57:20 +00:00
|
|
|
coqPackages_8_11 = mkCoqPackages coq_8_11;
|
2020-06-13 09:16:00 +01:00
|
|
|
coqPackages_8_12 = mkCoqPackages coq_8_12;
|
2020-12-09 07:32:51 +00:00
|
|
|
coqPackages_8_13 = mkCoqPackages coq_8_13;
|
2018-11-26 02:21:01 +00:00
|
|
|
coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
|
2020-08-16 07:24:33 +01:00
|
|
|
coqPackages_8_11
|
2018-11-26 02:21:01 +00:00
|
|
|
);
|
2017-12-15 19:52:16 +00:00
|
|
|
coq = coqPackages.coq;
|
|
|
|
|
|
|
|
}
|