coq-packages.nix

{
  lib,
  stdenv,
  fetchurl,
  fetchzip,
  callPackage,
  newScope,
  ocamlPackages_4_09,
  ocamlPackages_4_10,
  ocamlPackages_4_12,
  ocamlPackages_4_14,
  rocqPackages_9_0,
  rocqPackages_9_1,
  rocqPackages,
  fetchpatch,
  makeWrapper,
  coq2html,
}@args:
let
  lib = import ../build-support/coq/extra-lib.nix { inherit (args) lib; };
in
let
  mkCoqPackages' =
    self: coq:
    let
      callPackage = self.callPackage;
    in
    {
      inherit coq lib;
      coqPackages = self // {
        recurseForDerivations = false;
      };

      metaFetch = import ../build-support/coq/meta-fetch/default.nix {
        inherit
          lib
          stdenv
          fetchzip
          fetchurl
          ;
      };
      mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { });

      contribs = lib.recurseIntoAttrs (callPackage ../development/coq-modules/contribs { });

      aac-tactics = callPackage ../development/coq-modules/aac-tactics { };
      addition-chains = callPackage ../development/coq-modules/addition-chains { };
      async-test = callPackage ../development/coq-modules/async-test { };
      atbr = callPackage ../development/coq-modules/atbr { };
      autosubst = callPackage ../development/coq-modules/autosubst { };
      autosubst-ocaml = callPackage ../development/coq-modules/autosubst-ocaml { };
      bbv = callPackage ../development/coq-modules/bbv { };
      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 { };
      ceres = callPackage ../development/coq-modules/ceres { };
      Cheerios = callPackage ../development/coq-modules/Cheerios { };
      coinduction = callPackage ../development/coq-modules/coinduction { };
      CoLoR = callPackage ../development/coq-modules/CoLoR (
        lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
          bignums = self.bignums.override { version = "8.13.0"; };
        }
      );
      compcert = callPackage ../development/coq-modules/compcert {
        inherit
          fetchpatch
          makeWrapper
          coq2html
          lib
          stdenv
          ;
        ocamlPackages = ocamlPackages_4_14;
      };
      coq-bits = callPackage ../development/coq-modules/coq-bits { };
      coq-elpi = callPackage ../development/coq-modules/coq-elpi { };
      coq-hammer = callPackage ../development/coq-modules/coq-hammer { };
      coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { };
      CoqMatrix = callPackage ../development/coq-modules/coq-matrix { };
      coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
      coq-lsp = callPackage ../development/coq-modules/coq-lsp { };
      coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
      coq-tactical = callPackage ../development/coq-modules/coq-tactical { };
      coqeal = callPackage ../development/coq-modules/coqeal (
        lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
          bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
        }
      );
      coqhammer = callPackage ../development/coq-modules/coqhammer { };
      coqide = callPackage ../development/coq-modules/coqide { };
      coqprime = callPackage ../development/coq-modules/coqprime { };
      coqtail-math = callPackage ../development/coq-modules/coqtail-math { };
      coquelicot = callPackage ../development/coq-modules/coquelicot { };
      coqutil = callPackage ../development/coq-modules/coqutil { };
      coqfmt = callPackage ../development/coq-modules/coqfmt { };
      corn = callPackage ../development/coq-modules/corn { };
      deriving = callPackage ../development/coq-modules/deriving { };
      dpdgraph = callPackage ../development/coq-modules/dpdgraph { };
      ElmExtraction = callPackage ../development/coq-modules/ElmExtraction { };
      equations = callPackage ../development/coq-modules/equations { };
      ExtLib = callPackage ../development/coq-modules/ExtLib { };
      extructures = callPackage ../development/coq-modules/extructures { };
      fcsl-pcm = callPackage ../development/coq-modules/fcsl-pcm { };
      flocq = callPackage ../development/coq-modules/flocq { };
      fourcolor = callPackage ../development/coq-modules/fourcolor { };
      gaia = callPackage ../development/coq-modules/gaia { };
      gaia-hydras = callPackage ../development/coq-modules/gaia-hydras { };
      gappalib = callPackage ../development/coq-modules/gappalib { };
      goedel = callPackage ../development/coq-modules/goedel { };
      graph-theory = callPackage ../development/coq-modules/graph-theory { };
      heq = callPackage ../development/coq-modules/heq { };
      hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder { };
      high-school-geometry = callPackage ../development/coq-modules/high-school-geometry { };
      HoTT = callPackage ../development/coq-modules/HoTT { };
      http = callPackage ../development/coq-modules/http { };
      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 { };
      iris-named-props = callPackage ../development/coq-modules/iris-named-props { };
      itauto = callPackage ../development/coq-modules/itauto { };
      ITree = callPackage ../development/coq-modules/ITree { };
      itree-io = callPackage ../development/coq-modules/itree-io { };
      jasmin = callPackage ../development/coq-modules/jasmin { };
      json = callPackage ../development/coq-modules/json { };
      lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { };
      LibHyps = callPackage ../development/coq-modules/LibHyps { };
      libvalidsdp = self.validsdp.libvalidsdp;
      ltac2 = callPackage ../development/coq-modules/ltac2 { };
      math-classes = callPackage ../development/coq-modules/math-classes { };
      mathcomp = callPackage ../development/coq-modules/mathcomp { };
      ssreflect = self.mathcomp.ssreflect;
      mathcomp-boot = self.mathcomp.boot;
      mathcomp-order = self.mathcomp.order;
      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 { };
      mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { };
      mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { };
      mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
      mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { };
      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
      mathcomp-classical = self.mathcomp-analysis.classical;
      mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
      mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };
      mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo { };
      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed { };
      mathcomp-reals = self.mathcomp-analysis.reals;
      mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
      mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan { };
      mathcomp-word = callPackage ../development/coq-modules/mathcomp-word { };
      mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify { };
      MenhirLib = callPackage ../development/coq-modules/MenhirLib { };
      metacoq = callPackage ../development/coq-modules/metacoq { };
      metacoq-utils = self.metacoq.utils;
      metacoq-common = self.metacoq.common;
      metacoq-template-coq = self.metacoq.template-coq;
      metacoq-pcuic = self.metacoq.pcuic;
      metacoq-safechecker = self.metacoq.safechecker;
      metacoq-template-pcuic = self.metacoq.template-pcuic;
      metacoq-erasure = self.metacoq.erasure;
      metacoq-quotation = self.metacoq.quotation;
      metacoq-safechecker-plugin = self.metacoq.safechecker-plugin;
      metacoq-erasure-plugin = self.metacoq.erasure-plugin;
      metacoq-translations = self.metacoq.translations;
      metalib = callPackage ../development/coq-modules/metalib { };
      metarocq = callPackage ../development/coq-modules/metarocq { };
      metarocq-utils = self.metarocq.utils;
      metarocq-common = self.metarocq.common;
      metarocq-template-rocq = self.metarocq.template-rocq;
      metarocq-pcuic = self.metarocq.pcuic;
      metarocq-safechecker = self.metarocq.safechecker;
      metarocq-template-pcuic = self.metarocq.template-pcuic;
      metarocq-erasure = self.metarocq.erasure;
      metarocq-quotation = self.metarocq.quotation;
      metarocq-safechecker-plugin = self.metarocq.safechecker-plugin;
      metarocq-erasure-plugin = self.metarocq.erasure-plugin;
      metarocq-translations = self.metarocq.translations;
      mtac2 = callPackage ../development/coq-modules/mtac2 { };
      multinomials = callPackage ../development/coq-modules/multinomials { };
      odd-order = callPackage ../development/coq-modules/odd-order { };
      Ordinal = callPackage ../development/coq-modules/Ordinal { };
      paco = callPackage ../development/coq-modules/paco { };
      paramcoq = callPackage ../development/coq-modules/paramcoq { };
      parsec = callPackage ../development/coq-modules/parsec { };
      parseque = callPackage ../development/coq-modules/parseque { };
      pocklington = callPackage ../development/coq-modules/pocklington { };
      QuickChick = callPackage ../development/coq-modules/QuickChick { };
      reglang = callPackage ../development/coq-modules/reglang { };
      relation-algebra = callPackage ../development/coq-modules/relation-algebra { };
      rewriter = callPackage ../development/coq-modules/rewriter { };
      RustExtraction = callPackage ../development/coq-modules/RustExtraction { };
      semantics = callPackage ../development/coq-modules/semantics { };
      serapi = callPackage ../development/coq-modules/serapi { };
      simple-io = callPackage ../development/coq-modules/simple-io { };
      smpl = callPackage ../development/coq-modules/smpl { };
      smtcoq = callPackage ../development/coq-modules/smtcoq { };
      ssprove = callPackage ../development/coq-modules/ssprove { };
      stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
      stalmarck = self.stalmarck-tactic.stalmarck;
      stdlib = callPackage ../development/coq-modules/stdlib { };
      stdpp = callPackage ../development/coq-modules/stdpp { };
      StructTact = callPackage ../development/coq-modules/StructTact { };
      tlc = callPackage ../development/coq-modules/tlc { };
      topology = callPackage ../development/coq-modules/topology { };
      trakt = callPackage ../development/coq-modules/trakt { };
      unicoq = callPackage ../development/coq-modules/unicoq { };
      validsdp = callPackage ../development/coq-modules/validsdp { };
      vcfloat = callPackage ../development/coq-modules/vcfloat (
        lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
          interval = self.interval.override { version = "4.9.0"; };
        }
      );
      Velisarios = callPackage ../development/coq-modules/Velisarios { };
      Verdi = callPackage ../development/coq-modules/Verdi { };
      Vpl = callPackage ../development/coq-modules/Vpl { };
      VplTactic = callPackage ../development/coq-modules/VplTactic { };
      vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };
      VST = callPackage ../development/coq-modules/VST (
        (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {
          compcert = self.compcert.override {
            version =
              with lib.versions;
              lib.switch self.coq.version [
                {
                  case = range "8.19" "8.20";
                  out = "3.15";
                }
                {
                  case = range "8.15" "8.18";
                  out = "3.13.1";
                }
                {
                  case = isEq "8.14";
                  out = "3.11";
                }
              ] null;
          };
        })
        // (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
          ITree = self.ITree.override {
            version = "4.0.0";
            paco = self.paco.override { version = "4.1.2"; };
          };
        })
      );
      wasmcert = callPackage ../development/coq-modules/wasmcert { };
      waterproof = callPackage ../development/coq-modules/waterproof { };
      zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
      filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
    };

  filterCoqPackages =
    set:
    lib.listToAttrs (
      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)
    );
  mkCoq =
    version: rp:
    callPackage ../applications/science/logic/coq {
      inherit
        version
        ocamlPackages_4_09
        ocamlPackages_4_10
        ocamlPackages_4_12
        ocamlPackages_4_14
        ;
      rocqPackages = rp;
    };
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 (inspecting 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
    self.filterPackages (!coq.dontFilter or false);

  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" { };
  coq_8_14 = mkCoq "8.14" { };
  coq_8_15 = mkCoq "8.15" { };
  coq_8_16 = mkCoq "8.16" { };
  coq_8_17 = mkCoq "8.17" { };
  coq_8_18 = mkCoq "8.18" { };
  coq_8_19 = mkCoq "8.19" { };
  coq_8_20 = mkCoq "8.20" { };
  coq_9_0 = mkCoq "9.0" rocqPackages_9_0;
  coq_9_1 = mkCoq "9.1" rocqPackages_9_1;

  coqPackages_8_7 = mkCoqPackages coq_8_7;
  coqPackages_8_8 = mkCoqPackages coq_8_8;
  coqPackages_8_9 = mkCoqPackages coq_8_9;
  coqPackages_8_10 = mkCoqPackages coq_8_10;
  coqPackages_8_11 = mkCoqPackages coq_8_11;
  coqPackages_8_12 = mkCoqPackages coq_8_12;
  coqPackages_8_13 = mkCoqPackages coq_8_13;
  coqPackages_8_14 = mkCoqPackages coq_8_14;
  coqPackages_8_15 = mkCoqPackages coq_8_15;
  coqPackages_8_16 = mkCoqPackages coq_8_16;
  coqPackages_8_17 = mkCoqPackages coq_8_17;
  coqPackages_8_18 = mkCoqPackages coq_8_18;
  coqPackages_8_19 = mkCoqPackages coq_8_19;
  coqPackages_8_20 = mkCoqPackages coq_8_20;
  coqPackages_9_0 = mkCoqPackages coq_9_0;
  coqPackages_9_1 = mkCoqPackages coq_9_1;

  coqPackages = lib.recurseIntoAttrs coqPackages_9_0;
  coq = coqPackages.coq;
}