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