nixpkgs/pkgs/top-level/coq-packages.nix

135 lines
6.9 KiB
Nix
Raw Normal View History

2020-12-07 21:03:47 +00:00
{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
2020-08-28 21:05:46 +00:00
, ocamlPackages_4_10, compcert
}@args:
let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
let
mkCoqPackages' = self: coq:
let callPackage = self.callPackage; in {
2020-08-28 21:05:46 +00:00
inherit coq lib;
coqPackages = self;
2020-08-28 21:05:46 +00:00
mkCoqDerivation = callPackage ../build-support/coq {};
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 {};
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 {};
coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
2020-08-28 21:05:46 +00:00
coqeal = callPackage ../development/coq-modules/coqeal {};
coqhammer = callPackage ../development/coq-modules/coqhammer {};
coqprime = callPackage ../development/coq-modules/coqprime {};
2021-04-08 17:52:35 +00:00
coqtail-math = callPackage ../development/coq-modules/coqtail-math {};
coquelicot = callPackage ../development/coq-modules/coquelicot {};
2018-11-29 16:54:24 +00:00
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 {};
2021-03-12 17:31:11 +00:00
fourcolor = callPackage ../development/coq-modules/fourcolor {};
gappalib = callPackage ../development/coq-modules/gappalib {};
2021-05-08 17:17:50 +00:00
goedel = callPackage ../development/coq-modules/goedel {};
heq = callPackage ../development/coq-modules/heq {};
hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
HoTT = callPackage ../development/coq-modules/HoTT {};
2021-05-08 16:55:56 +00:00
hydra-battles = callPackage ../development/coq-modules/hydra-battles {};
interval = callPackage ../development/coq-modules/interval {};
InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
iris = callPackage ../development/coq-modules/iris {};
2021-04-14 08:33:05 +00:00
ITree = callPackage ../development/coq-modules/ITree { };
2019-05-22 09:42:06 +00:00
ltac2 = callPackage ../development/coq-modules/ltac2 {};
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;
mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
2020-08-28 21:05:46 +00:00
mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
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 {};
mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
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 { };
paco = callPackage ../development/coq-modules/paco {};
2019-02-11 09:04:26 +00:00
paramcoq = callPackage ../development/coq-modules/paramcoq {};
pocklington = callPackage ../development/coq-modules/pocklington {};
QuickChick = callPackage ../development/coq-modules/QuickChick {};
simple-io = callPackage ../development/coq-modules/simple-io { };
2018-05-15 20:48:20 +00:00
stdpp = callPackage ../development/coq-modules/stdpp { };
StructTact = callPackage ../development/coq-modules/StructTact {};
tlc = callPackage ../development/coq-modules/tlc {};
2018-10-24 00:08:56 +00:00
Velisarios = callPackage ../development/coq-modules/Velisarios {};
Verdi = callPackage ../development/coq-modules/Verdi {};
2021-04-30 06:49:33 +00:00
VST = callPackage ../development/coq-modules/VST (with lib.versions;
lib.switch coq.coq-version [
{ case = "8.11"; out = { compcert = compcert.override { coqPackages = self; version = "3.7"; }; }; }
{ case = range "8.12" "8.13"; out = { compcert = compcert.override { coqPackages = self; }; }; }
] {});
2020-08-28 21:05:46 +00:00
filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
};
2020-08-28 21:05:46 +00:00
filterCoqPackages = set:
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))
) (lib.attrNames set)
);
2020-08-28 21:05:46 +00:00
mkCoq = version: callPackage ../applications/science/logic/coq {
inherit version ocamlPackages_4_05 ocamlPackages_4_09 ocamlPackages_4_10;
};
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
2020-08-28 21:05:46 +00:00
self.filterPackages (! coq.dontFilter or false);
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";
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-05-07 06:39:29 +00:00
coqPackages = recurseIntoAttrs coqPackages_8_13;
coq = coqPackages.coq;
}