nixpkgs/pkgs/top-level/coq-packages.nix

144 lines
6.3 KiB
Nix
Raw Normal View History

2018-11-02 09:09:15 +00:00
{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05 }:
let
mkCoqPackages' = self: coq:
let callPackage = self.callPackage; in {
inherit coq;
coqPackages = self;
contribs = recurseIntoAttrs
(callPackage ../development/coq-modules/contribs {});
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 { };
Cheerios = callPackage ../development/coq-modules/Cheerios {};
CoLoR = callPackage ../development/coq-modules/CoLoR {};
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
coq-extensible-records = callPackage ../development/coq-modules/coq-extensible-records {};
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
coqhammer = callPackage ../development/coq-modules/coqhammer {};
coqprime = callPackage ../development/coq-modules/coqprime {};
coquelicot = callPackage ../development/coq-modules/coquelicot {};
2018-11-29 16:54:24 +00:00
corn = callPackage ../development/coq-modules/corn {};
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 {};
gappalib = callPackage ../development/coq-modules/gappalib {};
heq = callPackage ../development/coq-modules/heq {};
HoTT = callPackage ../development/coq-modules/HoTT {};
interval = callPackage ../development/coq-modules/interval {};
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
iris = callPackage ../development/coq-modules/iris {};
2019-05-22 09:42:06 +00:00
ltac2 = callPackage ../development/coq-modules/ltac2 {};
math-classes = callPackage ../development/coq-modules/math-classes { };
inherit (callPackage ../development/coq-modules/mathcomp { })
mathcompGen mathcompGenSingle ssreflect
mathcompCorePkgs mathcomp
mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra
mathcomp-solvable mathcomp-field mathcomp-character
mathcompCorePkgs_1_7 mathcomp_1_7
mathcomp-ssreflect_1_7 mathcomp-fingroup_1_7 mathcomp-algebra_1_7
mathcomp-solvable_1_7 mathcomp-field_1_7 mathcomp-character_1_7
mathcompCorePkgs_1_8 mathcomp_1_8
mathcomp-ssreflect_1_8 mathcomp-fingroup_1_8 mathcomp-algebra_1_8
mathcomp-solvable_1_8 mathcomp-field_1_8 mathcomp-character_1_8
mathcompCorePkgs_1_9 mathcomp_1_9
mathcomp-ssreflect_1_9 mathcomp-fingroup_1_9 mathcomp-algebra_1_9
mathcomp-solvable_1_9 mathcomp-field_1_9 mathcomp-character_1_9;
inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
mathcompExtraGen multinomials coqeal
mathcomp-finmap mathcomp-bigenough mathcomp-analysis
mathcomp-multinomials mathcomp-real-closed mathcomp-coqeal
mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis
mathcomp_1_7-multinomials mathcomp_1_7-real-closed
mathcomp_1_7-finmap_1_0
mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis
mathcomp_1_8-multinomials mathcomp_1_8-real-closed mathcomp_1_8-coqeal
mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
mathcomp_1_9-multinomials mathcomp_1_9-real-closed;
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 {};
QuickChick = callPackage ../development/coq-modules/QuickChick {};
simple-io = callPackage ../development/coq-modules/simple-io { };
2018-05-15 20:48:20 +00:00
stdpp = callPackage ../development/coq-modules/stdpp { };
StructTact = callPackage ../development/coq-modules/StructTact {};
tlc = callPackage ../development/coq-modules/tlc {};
2018-10-24 00:08:56 +00:00
Velisarios = callPackage ../development/coq-modules/Velisarios {};
Verdi = callPackage ../development/coq-modules/Verdi {};
};
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)
);
in rec {
/* 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.
*/
mkCoqPackages = coq:
let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in
if coq.dontFilter or false then self
else filterCoqPackages coq self;
coq_8_5 = callPackage ../applications/science/logic/coq {
2018-08-21 21:22:24 +00:00
ocamlPackages = ocamlPackages_4_05;
version = "8.5pl3";
};
2017-12-16 06:14:41 +00:00
coq_8_6 = callPackage ../applications/science/logic/coq {
2018-08-21 21:33:13 +00:00
ocamlPackages = ocamlPackages_4_05;
2017-12-16 06:14:41 +00:00
version = "8.6.1";
};
coq_8_7 = callPackage ../applications/science/logic/coq {
2018-02-16 07:12:01 +00:00
version = "8.7.2";
};
2018-03-21 14:00:47 +00:00
coq_8_8 = callPackage ../applications/science/logic/coq {
2018-09-26 20:26:39 +00: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 {
2019-05-22 09:04:19 +00:00
version = "8.9.1";
2018-11-02 09:09:15 +00:00
};
2019-05-14 08:31:49 +00:00
coq_8_10 = callPackage ../applications/science/logic/coq {
2019-07-14 12:24:52 +00:00
version = "8.10+beta2";
2019-05-14 08:31:49 +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 08:31:49 +00:00
coqPackages_8_10 = mkCoqPackages coq_8_10;
coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
coqPackages_8_8
);
coq = coqPackages.coq;
}