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