blob: 3fa3d30aa94a403cf024df5c2a4deed101d22255 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
{ 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-bits = callPackage ../development/coq-modules/coq-bits {};
coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
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 {};
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 {};
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 {};
paramcoq = callPackage ../development/coq-modules/paramcoq {};
QuickChick = callPackage ../development/coq-modules/QuickChick {};
simple-io = callPackage ../development/coq-modules/simple-io { };
stdpp = callPackage ../development/coq-modules/stdpp { };
StructTact = callPackage ../development/coq-modules/StructTact {};
tlc = callPackage ../development/coq-modules/tlc {};
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 {
ocamlPackages = ocamlPackages_4_05;
version = "8.5pl3";
};
coq_8_6 = callPackage ../applications/science/logic/coq {
ocamlPackages = ocamlPackages_4_05;
version = "8.6.1";
};
coq_8_7 = callPackage ../applications/science/logic/coq {
version = "8.7.2";
};
coq_8_8 = callPackage ../applications/science/logic/coq {
version = "8.8.2";
};
coq_8_9 = callPackage ../applications/science/logic/coq {
version = "8.9.1";
};
coq_8_10 = callPackage ../applications/science/logic/coq {
version = "8.10.2";
};
coq_8_11 = callPackage ../applications/science/logic/coq {
version = "8.11+beta1";
};
coqPackages_8_5 = mkCoqPackages coq_8_5;
coqPackages_8_6 = mkCoqPackages coq_8_6;
coqPackages_8_7 = mkCoqPackages coq_8_7;
coqPackages_8_8 = mkCoqPackages coq_8_8;
coqPackages_8_9 = mkCoqPackages coq_8_9;
coqPackages_8_10 = mkCoqPackages coq_8_10;
coqPackages_8_11 = mkCoqPackages coq_8_11;
coqPackages = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
coqPackages_8_9
);
coq = coqPackages.coq;
}
|