nixpkgs/pkgs/top-level/coq-packages.nix

{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05 }:

let
  mkCoqPackages' = self: coq:
    let callPackage = self.callPackage; in {
      inherit coq;
      coqPackages = self;

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

      autosubst = callPackage ../development/coq-modules/autosubst {};
      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 { };
      Cheerios = callPackage ../development/coq-modules/Cheerios {};
      CoLoR = callPackage ../development/coq-modules/CoLoR {};
      coq-bits = callPackage ../development/coq-modules/coq-bits {};
      coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
      coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
      coq-extensible-records = callPackage ../development/coq-modules/coq-extensible-records {};
      coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
      coqhammer = callPackage ../development/coq-modules/coqhammer {};
      coqprime = callPackage ../development/coq-modules/coqprime {};
      coquelicot = callPackage ../development/coq-modules/coquelicot {};
      corn = callPackage ../development/coq-modules/corn {};
      dpdgraph = callPackage ../development/coq-modules/dpdgraph {};
      equations = callPackage ../development/coq-modules/equations { };
      fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
      flocq = callPackage ../development/coq-modules/flocq {};
      gappalib = callPackage ../development/coq-modules/gappalib {};
      heq = callPackage ../development/coq-modules/heq {};
      hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {};
      HoTT = callPackage ../development/coq-modules/HoTT {};
      interval = callPackage ../development/coq-modules/interval {};
      InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {};
      iris = callPackage ../development/coq-modules/iris {};
      ltac2 = callPackage ../development/coq-modules/ltac2 {};
      math-classes = callPackage ../development/coq-modules/math-classes { };
      inherit (callPackage ../development/coq-modules/mathcomp {})
        mathcompGen mathcompGenSingle ssreflect

        mathcompCorePkgs mathcomp
        mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra
        mathcomp-solvable mathcomp-field mathcomp-character

        mathcompCorePkgs_1_7 mathcomp_1_7
        mathcomp-ssreflect_1_7 mathcomp-fingroup_1_7 mathcomp-algebra_1_7
        mathcomp-solvable_1_7 mathcomp-field_1_7 mathcomp-character_1_7

        mathcompCorePkgs_1_8 mathcomp_1_8
        mathcomp-ssreflect_1_8 mathcomp-fingroup_1_8 mathcomp-algebra_1_8
        mathcomp-solvable_1_8 mathcomp-field_1_8 mathcomp-character_1_8

        mathcompCorePkgs_1_9 mathcomp_1_9
        mathcomp-ssreflect_1_9 mathcomp-fingroup_1_9 mathcomp-algebra_1_9
        mathcomp-solvable_1_9 mathcomp-field_1_9 mathcomp-character_1_9

        mathcompCorePkgs_1_10 mathcomp_1_10
        mathcomp-ssreflect_1_10 mathcomp-fingroup_1_10 mathcomp-algebra_1_10
        mathcomp-solvable_1_10 mathcomp-field_1_10 mathcomp-character_1_10
        ;
      inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { })
        mathcompExtraGen multinomials coqeal

        mathcomp-finmap mathcomp-bigenough mathcomp-analysis
        mathcomp-multinomials mathcomp-real-closed mathcomp-coqeal

        mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis
        mathcomp_1_7-multinomials mathcomp_1_7-real-closed
        mathcomp_1_7-finmap_1_0

        mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis
        mathcomp_1_8-multinomials mathcomp_1_8-real-closed mathcomp_1_8-coqeal

        mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis
        mathcomp_1_9-multinomials mathcomp_1_9-real-closed;
      metalib = callPackage ../development/coq-modules/metalib { };
      paco = callPackage ../development/coq-modules/paco {};
      paramcoq = callPackage ../development/coq-modules/paramcoq {};
      QuickChick = callPackage ../development/coq-modules/QuickChick {};
      simple-io = callPackage ../development/coq-modules/simple-io { };
      stdpp = callPackage ../development/coq-modules/stdpp { };
      StructTact = callPackage ../development/coq-modules/StructTact {};
      tlc = callPackage ../development/coq-modules/tlc {};
      Velisarios = callPackage ../development/coq-modules/Velisarios {};
      Verdi = callPackage ../development/coq-modules/Verdi {};
    };

  filterCoqPackages = coq: set:
    lib.listToAttrs (
      lib.concatMap (name:
        let v = set.${name}; in
        let p = v.compatibleCoqVersions or (_: true); in
        lib.optional (p coq.coq-version)
          (lib.nameValuePair name (
            if lib.isAttrs v && v.recurseForDerivations or false
            then filterCoqPackages coq v
            else v))
      ) (lib.attrNames set)
    );

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 (inpecting 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
    if coq.dontFilter or false then self
    else filterCoqPackages coq self;

  coq_8_5 = callPackage ../applications/science/logic/coq {
    ocamlPackages = ocamlPackages_4_05;
    version = "8.5pl3";
  };
  coq_8_6 = callPackage ../applications/science/logic/coq {
    ocamlPackages = ocamlPackages_4_05;
    version = "8.6.1";
  };
  coq_8_7 = callPackage ../applications/science/logic/coq {
    version = "8.7.2";
  };
  coq_8_8 = callPackage ../applications/science/logic/coq {
    version = "8.8.2";
  };
  coq_8_9 = callPackage ../applications/science/logic/coq {
    version = "8.9.1";
  };
  coq_8_10 = callPackage ../applications/science/logic/coq {
    version = "8.10.2";
  };
  coq_8_11 = callPackage ../applications/science/logic/coq {
    version = "8.11.1";
  };

  coqPackages_8_5 = mkCoqPackages coq_8_5;
  coqPackages_8_6 = mkCoqPackages coq_8_6;
  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 = recurseIntoAttrs (lib.mapDerivationAttrset lib.dontDistribute
    coqPackages_8_9
  );
  coq = coqPackages.coq;

}