tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 stdenv,
4 fetchurl,
5 fetchzip,
6 callPackage,
7 newScope,
8 recurseIntoAttrs,
9 ocamlPackages_4_09,
10 ocamlPackages_4_10,
11 ocamlPackages_4_12,
12 ocamlPackages_4_14,
13 rocqPackages_9_0,
14 rocqPackages_9_1,
15 rocqPackages,
16 fetchpatch,
17 makeWrapper,
18 coq2html,
19}@args:
20let
21 lib = import ../build-support/coq/extra-lib.nix { inherit (args) lib; };
22in
23let
24 mkCoqPackages' =
25 self: coq:
26 let
27 callPackage = self.callPackage;
28 in
29 {
30 inherit coq lib;
31 coqPackages = self // {
32 recurseForDerivations = false;
33 };
34
35 metaFetch = import ../build-support/coq/meta-fetch/default.nix {
36 inherit
37 lib
38 stdenv
39 fetchzip
40 fetchurl
41 ;
42 };
43 mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { });
44
45 contribs = recurseIntoAttrs (callPackage ../development/coq-modules/contribs { });
46
47 aac-tactics = callPackage ../development/coq-modules/aac-tactics { };
48 addition-chains = callPackage ../development/coq-modules/addition-chains { };
49 async-test = callPackage ../development/coq-modules/async-test { };
50 atbr = callPackage ../development/coq-modules/atbr { };
51 autosubst = callPackage ../development/coq-modules/autosubst { };
52 autosubst-ocaml = callPackage ../development/coq-modules/autosubst-ocaml { };
53 bbv = callPackage ../development/coq-modules/bbv { };
54 bignums =
55 if lib.versionAtLeast coq.coq-version "8.6" then
56 callPackage ../development/coq-modules/bignums { }
57 else
58 null;
59 category-theory = callPackage ../development/coq-modules/category-theory { };
60 ceres = callPackage ../development/coq-modules/ceres { };
61 Cheerios = callPackage ../development/coq-modules/Cheerios { };
62 coinduction = callPackage ../development/coq-modules/coinduction { };
63 CoLoR = callPackage ../development/coq-modules/CoLoR (
64 (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
65 bignums = self.bignums.override { version = "8.13.0"; };
66 })
67 );
68 compcert = callPackage ../development/coq-modules/compcert {
69 inherit
70 fetchpatch
71 makeWrapper
72 coq2html
73 lib
74 stdenv
75 ;
76 ocamlPackages = ocamlPackages_4_14;
77 };
78 coq-bits = callPackage ../development/coq-modules/coq-bits { };
79 coq-elpi = callPackage ../development/coq-modules/coq-elpi { };
80 coq-hammer = callPackage ../development/coq-modules/coq-hammer { };
81 coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { };
82 CoqMatrix = callPackage ../development/coq-modules/coq-matrix { };
83 coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
84 coq-lsp = callPackage ../development/coq-modules/coq-lsp { };
85 coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
86 coq-tactical = callPackage ../development/coq-modules/coq-tactical { };
87 coqeal = callPackage ../development/coq-modules/coqeal (
88 (lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
89 bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
90 })
91 );
92 coqhammer = callPackage ../development/coq-modules/coqhammer { };
93 coqide = callPackage ../development/coq-modules/coqide { };
94 coqprime = callPackage ../development/coq-modules/coqprime { };
95 coqtail-math = callPackage ../development/coq-modules/coqtail-math { };
96 coquelicot = callPackage ../development/coq-modules/coquelicot { };
97 coqutil = callPackage ../development/coq-modules/coqutil { };
98 coqfmt = callPackage ../development/coq-modules/coqfmt { };
99 corn = callPackage ../development/coq-modules/corn { };
100 deriving = callPackage ../development/coq-modules/deriving { };
101 dpdgraph = callPackage ../development/coq-modules/dpdgraph { };
102 ElmExtraction = callPackage ../development/coq-modules/ElmExtraction { };
103 equations = callPackage ../development/coq-modules/equations { };
104 ExtLib = callPackage ../development/coq-modules/ExtLib { };
105 extructures = callPackage ../development/coq-modules/extructures { };
106 fcsl-pcm = callPackage ../development/coq-modules/fcsl-pcm { };
107 flocq = callPackage ../development/coq-modules/flocq { };
108 fourcolor = callPackage ../development/coq-modules/fourcolor { };
109 gaia = callPackage ../development/coq-modules/gaia { };
110 gaia-hydras = callPackage ../development/coq-modules/gaia-hydras { };
111 gappalib = callPackage ../development/coq-modules/gappalib { };
112 goedel = callPackage ../development/coq-modules/goedel { };
113 graph-theory = callPackage ../development/coq-modules/graph-theory { };
114 heq = callPackage ../development/coq-modules/heq { };
115 hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder { };
116 high-school-geometry = callPackage ../development/coq-modules/high-school-geometry { };
117 HoTT = callPackage ../development/coq-modules/HoTT { };
118 http = callPackage ../development/coq-modules/http { };
119 hydra-battles = callPackage ../development/coq-modules/hydra-battles { };
120 interval = callPackage ../development/coq-modules/interval { };
121 InfSeqExt = callPackage ../development/coq-modules/InfSeqExt { };
122 iris = callPackage ../development/coq-modules/iris { };
123 iris-named-props = callPackage ../development/coq-modules/iris-named-props { };
124 itauto = callPackage ../development/coq-modules/itauto { };
125 ITree = callPackage ../development/coq-modules/ITree { };
126 itree-io = callPackage ../development/coq-modules/itree-io { };
127 jasmin = callPackage ../development/coq-modules/jasmin { };
128 json = callPackage ../development/coq-modules/json { };
129 lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { };
130 LibHyps = callPackage ../development/coq-modules/LibHyps { };
131 ltac2 = callPackage ../development/coq-modules/ltac2 { };
132 math-classes = callPackage ../development/coq-modules/math-classes { };
133 mathcomp = callPackage ../development/coq-modules/mathcomp { };
134 ssreflect = self.mathcomp.ssreflect;
135 mathcomp-boot = self.mathcomp.boot;
136 mathcomp-order = self.mathcomp.order;
137 mathcomp-ssreflect = self.mathcomp.ssreflect;
138 mathcomp-fingroup = self.mathcomp.fingroup;
139 mathcomp-algebra = self.mathcomp.algebra;
140 mathcomp-solvable = self.mathcomp.solvable;
141 mathcomp-field = self.mathcomp.field;
142 mathcomp-character = self.mathcomp.character;
143 mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { };
144 mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { };
145 mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { };
146 mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
147 mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { };
148 mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
149 mathcomp-classical = self.mathcomp-analysis.classical;
150 mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
151 mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };
152 mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo { };
153 mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed { };
154 mathcomp-reals = self.mathcomp-analysis.reals;
155 mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
156 mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan { };
157 mathcomp-word = callPackage ../development/coq-modules/mathcomp-word { };
158 mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify { };
159 MenhirLib = callPackage ../development/coq-modules/MenhirLib { };
160 metacoq = callPackage ../development/coq-modules/metacoq { };
161 metacoq-utils = self.metacoq.utils;
162 metacoq-common = self.metacoq.common;
163 metacoq-template-coq = self.metacoq.template-coq;
164 metacoq-pcuic = self.metacoq.pcuic;
165 metacoq-safechecker = self.metacoq.safechecker;
166 metacoq-template-pcuic = self.metacoq.template-pcuic;
167 metacoq-erasure = self.metacoq.erasure;
168 metacoq-quotation = self.metacoq.quotation;
169 metacoq-safechecker-plugin = self.metacoq.safechecker-plugin;
170 metacoq-erasure-plugin = self.metacoq.erasure-plugin;
171 metacoq-translations = self.metacoq.translations;
172 metalib = callPackage ../development/coq-modules/metalib { };
173 metarocq = callPackage ../development/coq-modules/metarocq { };
174 metarocq-utils = self.metarocq.utils;
175 metarocq-common = self.metarocq.common;
176 metarocq-template-rocq = self.metarocq.template-rocq;
177 metarocq-pcuic = self.metarocq.pcuic;
178 metarocq-safechecker = self.metarocq.safechecker;
179 metarocq-template-pcuic = self.metarocq.template-pcuic;
180 metarocq-erasure = self.metarocq.erasure;
181 metarocq-quotation = self.metarocq.quotation;
182 metarocq-safechecker-plugin = self.metarocq.safechecker-plugin;
183 metarocq-erasure-plugin = self.metarocq.erasure-plugin;
184 metarocq-translations = self.metarocq.translations;
185 mtac2 = callPackage ../development/coq-modules/mtac2 { };
186 multinomials = callPackage ../development/coq-modules/multinomials { };
187 odd-order = callPackage ../development/coq-modules/odd-order { };
188 Ordinal = callPackage ../development/coq-modules/Ordinal { };
189 paco = callPackage ../development/coq-modules/paco { };
190 paramcoq = callPackage ../development/coq-modules/paramcoq { };
191 parsec = callPackage ../development/coq-modules/parsec { };
192 parseque = callPackage ../development/coq-modules/parseque { };
193 pocklington = callPackage ../development/coq-modules/pocklington { };
194 QuickChick = callPackage ../development/coq-modules/QuickChick { };
195 reglang = callPackage ../development/coq-modules/reglang { };
196 relation-algebra = callPackage ../development/coq-modules/relation-algebra { };
197 rewriter = callPackage ../development/coq-modules/rewriter { };
198 RustExtraction = callPackage ../development/coq-modules/RustExtraction { };
199 semantics = callPackage ../development/coq-modules/semantics { };
200 serapi = callPackage ../development/coq-modules/serapi { };
201 simple-io = callPackage ../development/coq-modules/simple-io { };
202 smpl = callPackage ../development/coq-modules/smpl { };
203 smtcoq = callPackage ../development/coq-modules/smtcoq { };
204 ssprove = callPackage ../development/coq-modules/ssprove { };
205 stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
206 stalmarck = self.stalmarck-tactic.stalmarck;
207 stdlib = callPackage ../development/coq-modules/stdlib { };
208 stdpp = callPackage ../development/coq-modules/stdpp { };
209 StructTact = callPackage ../development/coq-modules/StructTact { };
210 tlc = callPackage ../development/coq-modules/tlc { };
211 topology = callPackage ../development/coq-modules/topology { };
212 trakt = callPackage ../development/coq-modules/trakt { };
213 unicoq = callPackage ../development/coq-modules/unicoq { };
214 vcfloat = callPackage ../development/coq-modules/vcfloat (
215 lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
216 interval = self.interval.override { version = "4.9.0"; };
217 }
218 );
219 Velisarios = callPackage ../development/coq-modules/Velisarios { };
220 Verdi = callPackage ../development/coq-modules/Verdi { };
221 Vpl = callPackage ../development/coq-modules/Vpl { };
222 VplTactic = callPackage ../development/coq-modules/VplTactic { };
223 vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };
224 VST = callPackage ../development/coq-modules/VST (
225 (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {
226 compcert = self.compcert.override {
227 version =
228 with lib.versions;
229 lib.switch self.coq.version [
230 {
231 case = range "8.15" "8.18";
232 out = "3.13.1";
233 }
234 {
235 case = isEq "8.14";
236 out = "3.11";
237 }
238 ] null;
239 };
240 })
241 // (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
242 ITree = self.ITree.override {
243 version = "4.0.0";
244 paco = self.paco.override { version = "4.1.2"; };
245 };
246 })
247 );
248 waterproof = callPackage ../development/coq-modules/waterproof { };
249 zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
250 filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
251 };
252
253 filterCoqPackages =
254 set:
255 lib.listToAttrs (
256 lib.concatMap (
257 name:
258 let
259 v = set.${name} or null;
260 in
261 lib.optional (!v.meta.coqFilter or false) (
262 lib.nameValuePair name (
263 if lib.isAttrs v && v.recurseForDerivations or false then filterCoqPackages v else v
264 )
265 )
266 ) (lib.attrNames set)
267 );
268 mkCoq =
269 version: rp:
270 callPackage ../applications/science/logic/coq {
271 inherit
272 version
273 ocamlPackages_4_09
274 ocamlPackages_4_10
275 ocamlPackages_4_12
276 ocamlPackages_4_14
277 ;
278 rocqPackages = rp;
279 };
280in
281rec {
282
283 /*
284 The function `mkCoqPackages` takes as input a derivation for Coq and produces
285 a set of libraries built with that specific Coq. More libraries are known to
286 this function than what is compatible with that version of Coq. Therefore,
287 libraries that are not known to be compatible are removed (filtered out) from
288 the resulting set. For meta-programming purposes (inspecting the derivations
289 rather than building the libraries) this filtering can be disabled by setting
290 a `dontFilter` attribute into the Coq derivation.
291 */
292 mkCoqPackages =
293 coq:
294 let
295 self = lib.makeScope newScope (lib.flip mkCoqPackages' coq);
296 in
297 self.filterPackages (!coq.dontFilter or false);
298
299 coq_8_7 = mkCoq "8.7" { };
300 coq_8_8 = mkCoq "8.8" { };
301 coq_8_9 = mkCoq "8.9" { };
302 coq_8_10 = mkCoq "8.10" { };
303 coq_8_11 = mkCoq "8.11" { };
304 coq_8_12 = mkCoq "8.12" { };
305 coq_8_13 = mkCoq "8.13" { };
306 coq_8_14 = mkCoq "8.14" { };
307 coq_8_15 = mkCoq "8.15" { };
308 coq_8_16 = mkCoq "8.16" { };
309 coq_8_17 = mkCoq "8.17" { };
310 coq_8_18 = mkCoq "8.18" { };
311 coq_8_19 = mkCoq "8.19" { };
312 coq_8_20 = mkCoq "8.20" { };
313 coq_9_0 = mkCoq "9.0" rocqPackages_9_0;
314 coq_9_1 = mkCoq "9.1" rocqPackages_9_1;
315
316 coqPackages_8_7 = mkCoqPackages coq_8_7;
317 coqPackages_8_8 = mkCoqPackages coq_8_8;
318 coqPackages_8_9 = mkCoqPackages coq_8_9;
319 coqPackages_8_10 = mkCoqPackages coq_8_10;
320 coqPackages_8_11 = mkCoqPackages coq_8_11;
321 coqPackages_8_12 = mkCoqPackages coq_8_12;
322 coqPackages_8_13 = mkCoqPackages coq_8_13;
323 coqPackages_8_14 = mkCoqPackages coq_8_14;
324 coqPackages_8_15 = mkCoqPackages coq_8_15;
325 coqPackages_8_16 = mkCoqPackages coq_8_16;
326 coqPackages_8_17 = mkCoqPackages coq_8_17;
327 coqPackages_8_18 = mkCoqPackages coq_8_18;
328 coqPackages_8_19 = mkCoqPackages coq_8_19;
329 coqPackages_8_20 = mkCoqPackages coq_8_20;
330 coqPackages_9_0 = mkCoqPackages coq_9_0;
331 coqPackages_9_1 = mkCoqPackages coq_9_1;
332
333 coqPackages = recurseIntoAttrs coqPackages_9_0;
334 coq = coqPackages.coq;
335}