pkgs/top-level/coq-packages.nix

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