2021-02-19 18:34:30 +00:00
|
|
|
{ lib, stdenv, fetchzip
|
|
|
|
, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
|
2022-10-11 06:51:38 +00:00
|
|
|
, ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14
|
|
|
|
, fetchpatch, makeWrapper, coq2html
|
2020-08-28 21:05:46 +00:00
|
|
|
}@args:
|
|
|
|
let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
|
2017-12-15 19:52:16 +00:00
|
|
|
let
|
|
|
|
mkCoqPackages' = self: coq:
|
2019-06-16 19:59:06 +00:00
|
|
|
let callPackage = self.callPackage; in {
|
2020-08-28 21:05:46 +00:00
|
|
|
inherit coq lib;
|
2017-12-15 19:52:16 +00:00
|
|
|
coqPackages = self;
|
|
|
|
|
2021-02-19 18:34:30 +00:00
|
|
|
metaFetch = import ../build-support/coq/meta-fetch/default.nix
|
|
|
|
{inherit lib stdenv fetchzip; };
|
2022-08-29 05:41:03 +00:00
|
|
|
mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq {});
|
2020-08-28 21:05:46 +00:00
|
|
|
|
2017-12-22 16:56:20 +00:00
|
|
|
contribs = recurseIntoAttrs
|
|
|
|
(callPackage ../development/coq-modules/contribs {});
|
|
|
|
|
2021-05-09 15:49:12 +00:00
|
|
|
aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
|
2021-08-17 08:40:13 +00:00
|
|
|
addition-chains = callPackage ../development/coq-modules/addition-chains {};
|
2017-12-15 19:52:16 +00:00
|
|
|
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 { };
|
2021-09-15 10:54:46 +00:00
|
|
|
ceres = callPackage ../development/coq-modules/ceres {};
|
2018-11-20 23:16:27 +00:00
|
|
|
Cheerios = callPackage ../development/coq-modules/Cheerios {};
|
2017-12-15 19:52:16 +00:00
|
|
|
CoLoR = callPackage ../development/coq-modules/CoLoR {};
|
2021-06-14 12:21:41 +00:00
|
|
|
compcert = callPackage ../development/coq-modules/compcert {
|
|
|
|
inherit fetchpatch makeWrapper coq2html lib stdenv;
|
|
|
|
};
|
2019-10-22 18:19:45 +00:00
|
|
|
coq-bits = callPackage ../development/coq-modules/coq-bits {};
|
2019-08-06 09:15:37 +00:00
|
|
|
coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
|
2017-12-15 19:52:16 +00:00
|
|
|
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
|
|
|
|
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
|
2021-11-24 14:51:08 +00:00
|
|
|
coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
|
2020-08-28 21:05:46 +00:00
|
|
|
coqeal = callPackage ../development/coq-modules/coqeal {};
|
2019-03-22 09:10:55 +00:00
|
|
|
coqhammer = callPackage ../development/coq-modules/coqhammer {};
|
2022-07-06 18:40:19 +00:00
|
|
|
coqide = callPackage ../development/coq-modules/coqide {};
|
2018-10-01 09:49:11 +00:00
|
|
|
coqprime = callPackage ../development/coq-modules/coqprime {};
|
2021-04-08 17:52:35 +00:00
|
|
|
coqtail-math = callPackage ../development/coq-modules/coqtail-math {};
|
2017-12-15 19:52:16 +00:00
|
|
|
coquelicot = callPackage ../development/coq-modules/coquelicot {};
|
2018-11-29 16:54:24 +00:00
|
|
|
corn = callPackage ../development/coq-modules/corn {};
|
2021-10-19 19:52:17 +00:00
|
|
|
deriving = callPackage ../development/coq-modules/deriving {};
|
2017-12-15 19:52:16 +00:00
|
|
|
dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
|
|
|
|
equations = callPackage ../development/coq-modules/equations { };
|
2021-10-19 19:52:23 +00:00
|
|
|
extructures = callPackage ../development/coq-modules/extructures { };
|
2017-12-15 19:52:16 +00:00
|
|
|
fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
|
|
|
|
flocq = callPackage ../development/coq-modules/flocq {};
|
2021-03-12 17:31:11 +00:00
|
|
|
fourcolor = callPackage ../development/coq-modules/fourcolor {};
|
2021-08-17 08:07:59 +00:00
|
|
|
gaia = callPackage ../development/coq-modules/gaia {};
|
2021-10-18 09:42:52 +00:00
|
|
|
gaia-hydras = callPackage ../development/coq-modules/gaia-hydras {};
|
2019-06-13 15:25:38 +00:00
|
|
|
gappalib = callPackage ../development/coq-modules/gappalib {};
|
2021-05-08 17:17:50 +00:00
|
|
|
goedel = callPackage ../development/coq-modules/goedel {};
|
2021-05-09 16:25:17 +00:00
|
|
|
graph-theory = callPackage ../development/coq-modules/graph-theory {};
|
2017-12-15 19:52:16 +00:00
|
|
|
heq = callPackage ../development/coq-modules/heq {};
|
2020-03-10 14:21:07 +00:00
|
|
|
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
|
2017-12-15 19:52:16 +00:00
|
|
|
HoTT = callPackage ../development/coq-modules/HoTT {};
|
2021-05-08 16:55:56 +00:00
|
|
|
hydra-battles = callPackage ../development/coq-modules/hydra-battles {};
|
2017-12-15 19:52:16 +00:00
|
|
|
interval = callPackage ../development/coq-modules/interval {};
|
2018-11-20 23:16:27 +00:00
|
|
|
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
|
2018-05-22 17:26:32 +00:00
|
|
|
iris = callPackage ../development/coq-modules/iris {};
|
2021-07-01 10:47:16 +00:00
|
|
|
itauto = callPackage ../development/coq-modules/itauto { };
|
2021-04-14 08:33:05 +00:00
|
|
|
ITree = callPackage ../development/coq-modules/ITree { };
|
2022-02-03 13:21:13 +00:00
|
|
|
LibHyps = callPackage ../development/coq-modules/LibHyps {};
|
2019-05-22 09:42:06 +00:00
|
|
|
ltac2 = callPackage ../development/coq-modules/ltac2 {};
|
2017-12-15 19:52:16 +00:00
|
|
|
math-classes = callPackage ../development/coq-modules/math-classes { };
|
2020-08-28 21:05:46 +00:00
|
|
|
mathcomp = callPackage ../development/coq-modules/mathcomp {};
|
|
|
|
ssreflect = self.mathcomp.ssreflect;
|
|
|
|
mathcomp-ssreflect = self.mathcomp.ssreflect;
|
|
|
|
mathcomp-fingroup = self.mathcomp.fingroup;
|
|
|
|
mathcomp-algebra = self.mathcomp.algebra;
|
|
|
|
mathcomp-solvable = self.mathcomp.solvable;
|
|
|
|
mathcomp-field = self.mathcomp.field;
|
|
|
|
mathcomp-character = self.mathcomp.character;
|
2021-01-14 00:24:20 +00:00
|
|
|
mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
|
2020-08-28 21:05:46 +00:00
|
|
|
mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
|
2022-08-02 09:09:22 +00:00
|
|
|
mathcomp-classical = self.mathcomp-analysis.classical;
|
2020-08-28 21:05:46 +00:00
|
|
|
mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
|
|
|
|
mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
|
|
|
|
mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
|
2021-12-17 09:02:55 +00:00
|
|
|
mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {};
|
2021-05-10 13:30:05 +00:00
|
|
|
mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
|
2021-10-28 14:17:24 +00:00
|
|
|
mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
|
2022-05-03 07:26:34 +00:00
|
|
|
metacoq = callPackage ../development/coq-modules/metacoq { };
|
2022-09-06 13:55:48 +00:00
|
|
|
metacoq-template-coq = self.metacoq.template-coq;
|
|
|
|
metacoq-pcuic = self.metacoq.pcuic;
|
|
|
|
metacoq-safechecker = self.metacoq.safechecker;
|
|
|
|
metacoq-erasure = self.metacoq.erasure;
|
2017-12-15 19:52:16 +00:00
|
|
|
metalib = callPackage ../development/coq-modules/metalib { };
|
2020-08-28 21:05:46 +00:00
|
|
|
multinomials = callPackage ../development/coq-modules/multinomials {};
|
2021-03-30 08:34:14 +00:00
|
|
|
odd-order = callPackage ../development/coq-modules/odd-order { };
|
2017-12-15 19:52:16 +00:00
|
|
|
paco = callPackage ../development/coq-modules/paco {};
|
2019-02-11 09:04:26 +00:00
|
|
|
paramcoq = callPackage ../development/coq-modules/paramcoq {};
|
2021-09-15 10:55:00 +00:00
|
|
|
parsec = callPackage ../development/coq-modules/parsec {};
|
2021-05-08 17:01:39 +00:00
|
|
|
pocklington = callPackage ../development/coq-modules/pocklington {};
|
2017-12-15 19:52:16 +00:00
|
|
|
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
2021-06-07 17:22:36 +00:00
|
|
|
reglang = callPackage ../development/coq-modules/reglang {};
|
2021-05-09 15:49:35 +00:00
|
|
|
relation-algebra = callPackage ../development/coq-modules/relation-algebra {};
|
2021-06-20 08:57:51 +00:00
|
|
|
semantics = callPackage ../development/coq-modules/semantics {};
|
2021-06-09 13:15:11 +00:00
|
|
|
serapi = callPackage ../development/coq-modules/serapi {};
|
2018-12-03 14:45:03 +00:00
|
|
|
simple-io = callPackage ../development/coq-modules/simple-io { };
|
2021-11-07 00:55:25 +00:00
|
|
|
smpl = callPackage ../development/coq-modules/smpl { };
|
2022-02-28 21:33:47 +00:00
|
|
|
smtcoq = callPackage ../development/coq-modules/smtcoq { };
|
2018-05-15 20:48:20 +00:00
|
|
|
stdpp = callPackage ../development/coq-modules/stdpp { };
|
2018-11-20 23:16:27 +00:00
|
|
|
StructTact = callPackage ../development/coq-modules/StructTact {};
|
2017-12-19 14:26:11 +00:00
|
|
|
tlc = callPackage ../development/coq-modules/tlc {};
|
2021-05-09 16:03:43 +00:00
|
|
|
topology = callPackage ../development/coq-modules/topology {};
|
2022-02-28 21:33:12 +00:00
|
|
|
trakt = callPackage ../development/coq-modules/trakt {};
|
2018-10-24 00:08:56 +00:00
|
|
|
Velisarios = callPackage ../development/coq-modules/Velisarios {};
|
2018-11-20 23:16:27 +00:00
|
|
|
Verdi = callPackage ../development/coq-modules/Verdi {};
|
2022-02-09 05:19:54 +00:00
|
|
|
VST = callPackage ../development/coq-modules/VST {};
|
2021-05-24 12:44:44 +00:00
|
|
|
zorns-lemma = callPackage ../development/coq-modules/zorns-lemma {};
|
2020-08-28 21:05:46 +00:00
|
|
|
filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
|
2017-12-15 19:52:16 +00:00
|
|
|
};
|
|
|
|
|
2020-08-28 21:05:46 +00:00
|
|
|
filterCoqPackages = set:
|
2018-12-01 18:15:42 +00:00
|
|
|
lib.listToAttrs (
|
2020-08-28 21:05:46 +00:00
|
|
|
lib.concatMap (name: let v = set.${name} or null; in
|
|
|
|
lib.optional (! v.meta.coqFilter or false)
|
|
|
|
(lib.nameValuePair name (
|
|
|
|
if lib.isAttrs v && v.recurseForDerivations or false
|
|
|
|
then filterCoqPackages v
|
|
|
|
else v))
|
2018-12-01 18:15:42 +00:00
|
|
|
) (lib.attrNames set)
|
2017-12-15 19:52:16 +00:00
|
|
|
);
|
2020-08-28 21:05:46 +00:00
|
|
|
mkCoq = version: callPackage ../applications/science/logic/coq {
|
2021-11-24 10:33:29 +00:00
|
|
|
inherit version
|
|
|
|
ocamlPackages_4_05
|
|
|
|
ocamlPackages_4_09
|
|
|
|
ocamlPackages_4_10
|
|
|
|
ocamlPackages_4_12
|
2022-10-11 06:51:38 +00:00
|
|
|
ocamlPackages_4_14
|
2021-11-24 10:33:29 +00:00
|
|
|
;
|
2020-08-28 21:05:46 +00:00
|
|
|
};
|
2017-12-15 19:52:16 +00:00
|
|
|
in rec {
|
|
|
|
|
2018-11-04 17:39:09 +00:00
|
|
|
/* 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.
|
|
|
|
*/
|
2017-12-15 19:52:16 +00:00
|
|
|
mkCoqPackages = coq:
|
2019-04-08 23:07:42 +00:00
|
|
|
let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in
|
2020-08-28 21:05:46 +00:00
|
|
|
self.filterPackages (! coq.dontFilter or false);
|
2017-12-15 19:52:16 +00:00
|
|
|
|
2020-08-28 21:05:46 +00:00
|
|
|
coq_8_5 = mkCoq "8.5";
|
|
|
|
coq_8_6 = mkCoq "8.6";
|
|
|
|
coq_8_7 = mkCoq "8.7";
|
|
|
|
coq_8_8 = mkCoq "8.8";
|
|
|
|
coq_8_9 = mkCoq "8.9";
|
|
|
|
coq_8_10 = mkCoq "8.10";
|
|
|
|
coq_8_11 = mkCoq "8.11";
|
|
|
|
coq_8_12 = mkCoq "8.12";
|
|
|
|
coq_8_13 = mkCoq "8.13";
|
2021-09-27 19:52:40 +00:00
|
|
|
coq_8_14 = mkCoq "8.14";
|
2021-12-08 17:06:40 +00:00
|
|
|
coq_8_15 = mkCoq "8.15";
|
2022-06-08 12:38:58 +00:00
|
|
|
coq_8_16 = mkCoq "8.16";
|
2017-12-15 19:52:16 +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;
|
2019-12-07 07:57:20 +00:00
|
|
|
coqPackages_8_11 = mkCoqPackages coq_8_11;
|
2020-06-13 08:16:00 +00:00
|
|
|
coqPackages_8_12 = mkCoqPackages coq_8_12;
|
2020-12-09 07:32:51 +00:00
|
|
|
coqPackages_8_13 = mkCoqPackages coq_8_13;
|
2021-09-27 19:52:40 +00:00
|
|
|
coqPackages_8_14 = mkCoqPackages coq_8_14;
|
2021-12-08 17:06:40 +00:00
|
|
|
coqPackages_8_15 = mkCoqPackages coq_8_15;
|
2022-06-08 12:38:58 +00:00
|
|
|
coqPackages_8_16 = mkCoqPackages coq_8_16;
|
2022-05-07 05:29:49 +00:00
|
|
|
coqPackages = recurseIntoAttrs coqPackages_8_15;
|
2017-12-15 19:52:16 +00:00
|
|
|
coq = coqPackages.coq;
|
|
|
|
|
|
|
|
}
|