pkgs/top-level/coq-packages.nix

   1 { lib, stdenv, fetchzip
   2 , callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
   3 , ocamlPackages_4_10, ocamlPackages_4_12, ocamlPackages_4_14
   4 , fetchpatch, makeWrapper, coq2html
   5 }@args:
   6 let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
   7 let
   8   mkCoqPackages' = self: coq:
   9     let callPackage = self.callPackage; in {
  10       inherit coq lib;
  11       coqPackages = self // { coqPackages = self.coqPackages // { recurseForDerivations = false; }; };
  12
  13       metaFetch = import ../build-support/coq/meta-fetch/default.nix
  14         {inherit lib stdenv fetchzip; };
  15       mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq {});
  16
  17       contribs = recurseIntoAttrs
  18         (callPackage ../development/coq-modules/contribs {});
  19
  20       aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
  21       addition-chains = callPackage ../development/coq-modules/addition-chains {};
  22       autosubst = callPackage ../development/coq-modules/autosubst {};
  23       bignums = if lib.versionAtLeast coq.coq-version "8.6"
  24         then callPackage ../development/coq-modules/bignums {}
  25         else null;
  26       category-theory = callPackage ../development/coq-modules/category-theory { };
  27       ceres = callPackage ../development/coq-modules/ceres {};
  28       Cheerios = callPackage ../development/coq-modules/Cheerios {};
  29       CoLoR = callPackage ../development/coq-modules/CoLoR (
  30         (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
  31           bignums = self.bignums.override { version = "8.13.0"; };
  32         })
  33       );
  34       compcert = callPackage ../development/coq-modules/compcert {
  35         inherit fetchpatch makeWrapper coq2html lib stdenv;
  36         ocamlPackages = ocamlPackages_4_14;
  37       };
  38       coq-bits = callPackage ../development/coq-modules/coq-bits {};
  39       coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
  40       coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
  41       coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
  42       coq-lsp = callPackage ../development/coq-modules/coq-lsp {};
  43       coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
  44       coqeal = callPackage ../development/coq-modules/coqeal (
  45         (lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
  46           bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
  47         })
  48       );
  49       coqhammer = callPackage ../development/coq-modules/coqhammer {};
  50       coqide = callPackage ../development/coq-modules/coqide {};
  51       coqprime = callPackage ../development/coq-modules/coqprime {};
  52       coqtail-math = callPackage ../development/coq-modules/coqtail-math {};
  53       coquelicot = callPackage ../development/coq-modules/coquelicot {};
  54       corn = callPackage ../development/coq-modules/corn {};
  55       deriving = callPackage ../development/coq-modules/deriving {};
  56       dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
  57       equations = callPackage ../development/coq-modules/equations { };
  58       extructures = callPackage ../development/coq-modules/extructures { };
  59       fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
  60       flocq = callPackage ../development/coq-modules/flocq {};
  61       fourcolor = callPackage ../development/coq-modules/fourcolor {};
  62       gaia = callPackage ../development/coq-modules/gaia {};
  63       gaia-hydras = callPackage ../development/coq-modules/gaia-hydras {};
  64       gappalib = callPackage ../development/coq-modules/gappalib {};
  65       goedel = callPackage ../development/coq-modules/goedel {};
  66       graph-theory = callPackage ../development/coq-modules/graph-theory {};
  67       heq = callPackage ../development/coq-modules/heq {};
  68       hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
  69       HoTT = callPackage ../development/coq-modules/HoTT {};
  70       hydra-battles = callPackage ../development/coq-modules/hydra-battles {};
  71       interval = callPackage ../development/coq-modules/interval {};
  72       InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
  73       iris = callPackage ../development/coq-modules/iris {};
  74       iris-named-props = callPackage ../development/coq-modules/iris-named-props {};
  75       itauto = callPackage ../development/coq-modules/itauto { };
  76       ITree = callPackage ../development/coq-modules/ITree { };
  77       LibHyps = callPackage ../development/coq-modules/LibHyps {};
  78       ltac2 = callPackage ../development/coq-modules/ltac2 {};
  79       math-classes = callPackage ../development/coq-modules/math-classes { };
  80       mathcomp = callPackage ../development/coq-modules/mathcomp {};
  81       ssreflect          = self.mathcomp.ssreflect;
  82       mathcomp-ssreflect = self.mathcomp.ssreflect;
  83       mathcomp-fingroup  = self.mathcomp.fingroup;
  84       mathcomp-algebra   = self.mathcomp.algebra;
  85       mathcomp-solvable  = self.mathcomp.solvable;
  86       mathcomp-field     = self.mathcomp.field;
  87       mathcomp-character = self.mathcomp.character;
  88       mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
  89       mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics {};
  90       mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
  91       mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery {};
  92       mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
  93       mathcomp-classical = self.mathcomp-analysis.classical;
  94       mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
  95       mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo {};
  96       mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
  97       mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
  98       mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {};
  99       mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
 100       metacoq = callPackage ../development/coq-modules/metacoq { };
 101       metacoq-template-coq = self.metacoq.template-coq;
 102       metacoq-pcuic        = self.metacoq.pcuic;
 103       metacoq-safechecker  = self.metacoq.safechecker;
 104       metacoq-erasure      = self.metacoq.erasure;
 105       metalib = callPackage ../development/coq-modules/metalib { };
 106       multinomials = callPackage ../development/coq-modules/multinomials {};
 107       odd-order = callPackage ../development/coq-modules/odd-order { };
 108       paco = callPackage ../development/coq-modules/paco {};
 109       paramcoq = callPackage ../development/coq-modules/paramcoq {};
 110       parsec = callPackage ../development/coq-modules/parsec {};
 111       pocklington = callPackage ../development/coq-modules/pocklington {};
 112       QuickChick = callPackage ../development/coq-modules/QuickChick {};
 113       reglang = callPackage ../development/coq-modules/reglang {};
 114       relation-algebra = callPackage ../development/coq-modules/relation-algebra {};
 115       semantics = callPackage ../development/coq-modules/semantics {};
 116       serapi = callPackage ../development/coq-modules/serapi {};
 117       simple-io = callPackage ../development/coq-modules/simple-io { };
 118       smpl = callPackage ../development/coq-modules/smpl { };
 119       smtcoq = callPackage ../development/coq-modules/smtcoq { };
 120       stdpp = callPackage ../development/coq-modules/stdpp { };
 121       StructTact = callPackage ../development/coq-modules/StructTact {};
 122       tlc = callPackage ../development/coq-modules/tlc {};
 123       topology = callPackage ../development/coq-modules/topology {};
 124       trakt = callPackage ../development/coq-modules/trakt {};
 125       vcfloat = callPackage ../development/coq-modules/vcfloat (lib.optionalAttrs
 126         (lib.versions.range "8.16" "8.18" self.coq.version) {
 127           interval = self.interval.override { version = "4.9.0"; };
 128         });
 129       Velisarios = callPackage ../development/coq-modules/Velisarios {};
 130       Verdi = callPackage ../development/coq-modules/Verdi {};
 131       Vpl = callPackage ../development/coq-modules/Vpl {};
 132       VplTactic = callPackage ../development/coq-modules/VplTactic {};
 133       vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server {};
 134       VST = callPackage ../development/coq-modules/VST ((lib.optionalAttrs
 135         (lib.versionAtLeast self.coq.version "8.14") {
 136           compcert = self.compcert.override {
 137             version = with lib.versions; lib.switch self.coq.version [
 138               { case = range "8.15" "8.17"; out = "3.13.1"; }
 139               { case = isEq "8.14"; out = "3.11"; }
 140             ] null;
 141           };
 142         }) // (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
 143           ITree = self.ITree.override {
 144             version = "4.0.0";
 145             paco = self.paco.override { version = "4.1.2"; };
 146           };
 147        }));
 148       zorns-lemma = callPackage ../development/coq-modules/zorns-lemma {};
 149       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
 150     };
 151
 152   filterCoqPackages = set:
 153     lib.listToAttrs (
 154       lib.concatMap (name: let v = set.${name} or null; in
 155           lib.optional (! v.meta.coqFilter or false)
 156             (lib.nameValuePair name (
 157               if lib.isAttrs v && v.recurseForDerivations or false
 158               then filterCoqPackages v
 159               else v))
 160       ) (lib.attrNames set)
 161     );
 162   mkCoq = version: callPackage ../applications/science/logic/coq {
 163     inherit version
 164       ocamlPackages_4_05
 165       ocamlPackages_4_09
 166       ocamlPackages_4_10
 167       ocamlPackages_4_12
 168       ocamlPackages_4_14
 169     ;
 170   };
 171 in rec {
 172
 173   /* The function `mkCoqPackages` takes as input a derivation for Coq and produces
 174    * a set of libraries built with that specific Coq. More libraries are known to
 175    * this function than what is compatible with that version of Coq. Therefore,
 176    * libraries that are not known to be compatible are removed (filtered out) from
 177    * the resulting set. For meta-programming purposes (inpecting the derivations
 178    * rather than building the libraries) this filtering can be disabled by setting
 179    * a `dontFilter` attribute into the Coq derivation.
 180    */
 181   mkCoqPackages = coq:
 182     let self = lib.makeScope newScope (lib.flip mkCoqPackages' coq); in
 183     self.filterPackages (! coq.dontFilter or false);
 184
 185   coq_8_5  = mkCoq "8.5";
 186   coq_8_6  = mkCoq "8.6";
 187   coq_8_7  = mkCoq "8.7";
 188   coq_8_8  = mkCoq "8.8";
 189   coq_8_9  = mkCoq "8.9";
 190   coq_8_10 = mkCoq "8.10";
 191   coq_8_11 = mkCoq "8.11";
 192   coq_8_12 = mkCoq "8.12";
 193   coq_8_13 = mkCoq "8.13";
 194   coq_8_14 = mkCoq "8.14";
 195   coq_8_15 = mkCoq "8.15";
 196   coq_8_16 = mkCoq "8.16";
 197   coq_8_17 = mkCoq "8.17";
 198   coq_8_18 = mkCoq "8.18";
 199   coq_8_19 = mkCoq "8.19";
 200
 201   coqPackages_8_5 = mkCoqPackages coq_8_5 // { __attrsFailEvaluation = true; };
 202   coqPackages_8_6 = mkCoqPackages coq_8_6 // { __attrsFailEvaluation = true; };
 203   coqPackages_8_7 = mkCoqPackages coq_8_7 // { __attrsFailEvaluation = true; };
 204   coqPackages_8_8 = mkCoqPackages coq_8_8 // { __attrsFailEvaluation = true; };
 205   coqPackages_8_9 = mkCoqPackages coq_8_9 // { __attrsFailEvaluation = true; };
 206   coqPackages_8_10 = mkCoqPackages coq_8_10 // { __attrsFailEvaluation = true; };
 207   coqPackages_8_11 = mkCoqPackages coq_8_11 // { __attrsFailEvaluation = true; };
 208   coqPackages_8_12 = mkCoqPackages coq_8_12 // { __attrsFailEvaluation = true; };
 209   coqPackages_8_13 = mkCoqPackages coq_8_13 // { __attrsFailEvaluation = true; };
 210   coqPackages_8_14 = mkCoqPackages coq_8_14 // { __attrsFailEvaluation = true; };
 211   coqPackages_8_15 = mkCoqPackages coq_8_15 // { __attrsFailEvaluation = true; };
 212   coqPackages_8_16 = mkCoqPackages coq_8_16 // { __attrsFailEvaluation = true; };
 213   coqPackages_8_17 = mkCoqPackages coq_8_17 // { __attrsFailEvaluation = true; };
 214   coqPackages_8_18 = mkCoqPackages coq_8_18 // { __attrsFailEvaluation = true; };
 215   coqPackages_8_19 = mkCoqPackages coq_8_19 // { __attrsFailEvaluation = true; };
 216   coqPackages =
 217     let cp = recurseIntoAttrs coqPackages_8_18;
 218     in cp // { coqPackages = cp.coqPackages // { __attrsFailEvaluation = true; }; } // { __recurseIntoDerivationForReleaseJobs = true; };
 219   coq = coqPackages.coq;
 220
 221 }