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