pkgs/top-level/coq-packages.nix at deb7674d713537dc08757396d8e1b71611dea73b · pyrox.dev/nixpkgs

pyrox.dev / nixpkgs
lol
nixpkgs / pkgs / top-level / coq-packages.nix
at deb7674d713537dc08757396d8e1b71611dea73b 16 kB view raw
  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      libvalidsdp = self.validsdp.libvalidsdp;
132      ltac2 = callPackage ../development/coq-modules/ltac2 { };
133      math-classes = callPackage ../development/coq-modules/math-classes { };
134      mathcomp = callPackage ../development/coq-modules/mathcomp { };
135      ssreflect = self.mathcomp.ssreflect;
136      mathcomp-boot = self.mathcomp.boot;
137      mathcomp-order = self.mathcomp.order;
138      mathcomp-ssreflect = self.mathcomp.ssreflect;
139      mathcomp-fingroup = self.mathcomp.fingroup;
140      mathcomp-algebra = self.mathcomp.algebra;
141      mathcomp-solvable = self.mathcomp.solvable;
142      mathcomp-field = self.mathcomp.field;
143      mathcomp-character = self.mathcomp.character;
144      mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { };
145      mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { };
146      mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { };
147      mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
148      mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { };
149      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
150      mathcomp-classical = self.mathcomp-analysis.classical;
151      mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
152      mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };
153      mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo { };
154      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed { };
155      mathcomp-reals = self.mathcomp-analysis.reals;
156      mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
157      mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan { };
158      mathcomp-word = callPackage ../development/coq-modules/mathcomp-word { };
159      mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify { };
160      MenhirLib = callPackage ../development/coq-modules/MenhirLib { };
161      metacoq = callPackage ../development/coq-modules/metacoq { };
162      metacoq-utils = self.metacoq.utils;
163      metacoq-common = self.metacoq.common;
164      metacoq-template-coq = self.metacoq.template-coq;
165      metacoq-pcuic = self.metacoq.pcuic;
166      metacoq-safechecker = self.metacoq.safechecker;
167      metacoq-template-pcuic = self.metacoq.template-pcuic;
168      metacoq-erasure = self.metacoq.erasure;
169      metacoq-quotation = self.metacoq.quotation;
170      metacoq-safechecker-plugin = self.metacoq.safechecker-plugin;
171      metacoq-erasure-plugin = self.metacoq.erasure-plugin;
172      metacoq-translations = self.metacoq.translations;
173      metalib = callPackage ../development/coq-modules/metalib { };
174      metarocq = callPackage ../development/coq-modules/metarocq { };
175      metarocq-utils = self.metarocq.utils;
176      metarocq-common = self.metarocq.common;
177      metarocq-template-rocq = self.metarocq.template-rocq;
178      metarocq-pcuic = self.metarocq.pcuic;
179      metarocq-safechecker = self.metarocq.safechecker;
180      metarocq-template-pcuic = self.metarocq.template-pcuic;
181      metarocq-erasure = self.metarocq.erasure;
182      metarocq-quotation = self.metarocq.quotation;
183      metarocq-safechecker-plugin = self.metarocq.safechecker-plugin;
184      metarocq-erasure-plugin = self.metarocq.erasure-plugin;
185      metarocq-translations = self.metarocq.translations;
186      mtac2 = callPackage ../development/coq-modules/mtac2 { };
187      multinomials = callPackage ../development/coq-modules/multinomials { };
188      odd-order = callPackage ../development/coq-modules/odd-order { };
189      Ordinal = callPackage ../development/coq-modules/Ordinal { };
190      paco = callPackage ../development/coq-modules/paco { };
191      paramcoq = callPackage ../development/coq-modules/paramcoq { };
192      parsec = callPackage ../development/coq-modules/parsec { };
193      parseque = callPackage ../development/coq-modules/parseque { };
194      pocklington = callPackage ../development/coq-modules/pocklington { };
195      QuickChick = callPackage ../development/coq-modules/QuickChick { };
196      reglang = callPackage ../development/coq-modules/reglang { };
197      relation-algebra = callPackage ../development/coq-modules/relation-algebra { };
198      rewriter = callPackage ../development/coq-modules/rewriter { };
199      RustExtraction = callPackage ../development/coq-modules/RustExtraction { };
200      semantics = callPackage ../development/coq-modules/semantics { };
201      serapi = callPackage ../development/coq-modules/serapi { };
202      simple-io = callPackage ../development/coq-modules/simple-io { };
203      smpl = callPackage ../development/coq-modules/smpl { };
204      smtcoq = callPackage ../development/coq-modules/smtcoq { };
205      ssprove = callPackage ../development/coq-modules/ssprove { };
206      stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
207      stalmarck = self.stalmarck-tactic.stalmarck;
208      stdlib = callPackage ../development/coq-modules/stdlib { };
209      stdpp = callPackage ../development/coq-modules/stdpp { };
210      StructTact = callPackage ../development/coq-modules/StructTact { };
211      tlc = callPackage ../development/coq-modules/tlc { };
212      topology = callPackage ../development/coq-modules/topology { };
213      trakt = callPackage ../development/coq-modules/trakt { };
214      unicoq = callPackage ../development/coq-modules/unicoq { };
215      validsdp = callPackage ../development/coq-modules/validsdp { };
216      vcfloat = callPackage ../development/coq-modules/vcfloat (
217        lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
218          interval = self.interval.override { version = "4.9.0"; };
219        }
220      );
221      Velisarios = callPackage ../development/coq-modules/Velisarios { };
222      Verdi = callPackage ../development/coq-modules/Verdi { };
223      Vpl = callPackage ../development/coq-modules/Vpl { };
224      VplTactic = callPackage ../development/coq-modules/VplTactic { };
225      vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };
226      VST = callPackage ../development/coq-modules/VST (
227        (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {
228          compcert = self.compcert.override {
229            version =
230              with lib.versions;
231              lib.switch self.coq.version [
232                {
233                  case = range "8.19" "8.20";
234                  out = "3.15";
235                }
236                {
237                  case = range "8.15" "8.18";
238                  out = "3.13.1";
239                }
240                {
241                  case = isEq "8.14";
242                  out = "3.11";
243                }
244              ] null;
245          };
246        })
247        // (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
248          ITree = self.ITree.override {
249            version = "4.0.0";
250            paco = self.paco.override { version = "4.1.2"; };
251          };
252        })
253      );
254      wasmcert = callPackage ../development/coq-modules/wasmcert { };
255      waterproof = callPackage ../development/coq-modules/waterproof { };
256      zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
257      filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
258    };
259
260  filterCoqPackages =
261    set:
262    lib.listToAttrs (
263      lib.concatMap (
264        name:
265        let
266          v = set.${name} or null;
267        in
268        lib.optional (!v.meta.coqFilter or false) (
269          lib.nameValuePair name (
270            if lib.isAttrs v && v.recurseForDerivations or false then filterCoqPackages v else v
271          )
272        )
273      ) (lib.attrNames set)
274    );
275  mkCoq =
276    version: rp:
277    callPackage ../applications/science/logic/coq {
278      inherit
279        version
280        ocamlPackages_4_09
281        ocamlPackages_4_10
282        ocamlPackages_4_12
283        ocamlPackages_4_14
284        ;
285      rocqPackages = rp;
286    };
287in
288rec {
289
290  /*
291    The function `mkCoqPackages` takes as input a derivation for Coq and produces
292    a set of libraries built with that specific Coq. More libraries are known to
293    this function than what is compatible with that version of Coq. Therefore,
294    libraries that are not known to be compatible are removed (filtered out) from
295    the resulting set. For meta-programming purposes (inspecting the derivations
296    rather than building the libraries) this filtering can be disabled by setting
297    a `dontFilter` attribute into the Coq derivation.
298  */
299  mkCoqPackages =
300    coq:
301    let
302      self = lib.makeScope newScope (lib.flip mkCoqPackages' coq);
303    in
304    self.filterPackages (!coq.dontFilter or false);
305
306  coq_8_7 = mkCoq "8.7" { };
307  coq_8_8 = mkCoq "8.8" { };
308  coq_8_9 = mkCoq "8.9" { };
309  coq_8_10 = mkCoq "8.10" { };
310  coq_8_11 = mkCoq "8.11" { };
311  coq_8_12 = mkCoq "8.12" { };
312  coq_8_13 = mkCoq "8.13" { };
313  coq_8_14 = mkCoq "8.14" { };
314  coq_8_15 = mkCoq "8.15" { };
315  coq_8_16 = mkCoq "8.16" { };
316  coq_8_17 = mkCoq "8.17" { };
317  coq_8_18 = mkCoq "8.18" { };
318  coq_8_19 = mkCoq "8.19" { };
319  coq_8_20 = mkCoq "8.20" { };
320  coq_9_0 = mkCoq "9.0" rocqPackages_9_0;
321  coq_9_1 = mkCoq "9.1" rocqPackages_9_1;
322
323  coqPackages_8_7 = mkCoqPackages coq_8_7;
324  coqPackages_8_8 = mkCoqPackages coq_8_8;
325  coqPackages_8_9 = mkCoqPackages coq_8_9;
326  coqPackages_8_10 = mkCoqPackages coq_8_10;
327  coqPackages_8_11 = mkCoqPackages coq_8_11;
328  coqPackages_8_12 = mkCoqPackages coq_8_12;
329  coqPackages_8_13 = mkCoqPackages coq_8_13;
330  coqPackages_8_14 = mkCoqPackages coq_8_14;
331  coqPackages_8_15 = mkCoqPackages coq_8_15;
332  coqPackages_8_16 = mkCoqPackages coq_8_16;
333  coqPackages_8_17 = mkCoqPackages coq_8_17;
334  coqPackages_8_18 = mkCoqPackages coq_8_18;
335  coqPackages_8_19 = mkCoqPackages coq_8_19;
336  coqPackages_8_20 = mkCoqPackages coq_8_20;
337  coqPackages_9_0 = mkCoqPackages coq_9_0;
338  coqPackages_9_1 = mkCoqPackages coq_9_1;
339
340  coqPackages = recurseIntoAttrs coqPackages_9_0;
341  coq = coqPackages.coq;
342}