Test CI

.nix/config.nix

@@ -0,0 +1,228 @@
+with builtins; with (import <nixpkgs> {}).lib;
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  ## The attribute to build from the local sources,
+  ## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
+  ## Will determine the default main-job of the bundles defined below
+  attribute = "stdlib";
+
+  ## If you want to select a different attribute (to build from the local sources as well)
+  ## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
+  # shell-attribute = "{{nix_name}}";
+
+  ## Maybe the shortname of the library is different from
+  ## the name of the nixpkgs attribute, if so, set it here:
+  # pname = "{{shortname}}";
+
+  ## Lists the dependencies, phrased in terms of nix attributes.
+  ## No need to list Coq, it is already included.
+  ## These dependencies will systematically be added to the currently
+  ## known dependencies, if any more than Coq.
+  ## /!\ Remove this field as soon as the package is available on nixpkgs.
+  ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
+  # buildInputs = [ ];
+
+  ## Indicate the relative location of your _CoqProject
+  ## If not specified, it defaults to "_CoqProject"
+  coqproject = "theories/_CoqProject";
+
+  ## Cachix caches to use in CI
+  ## Below we list some standard ones
+  cachix.coq = {};
+  cachix.math-comp = {};
+  # cachix.coq-community = {};
+
+  ## If you have write access to one of these caches you can
+  ## provide the auth token or signing key through a secret
+  ## variable on GitHub. Then, you should give the variable
+  ## name here. For instance, coq-community projects can use
+  ## the following line instead of the one above:
+  cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
+
+  ## Or if you have a signing key for a given Cachix cache:
+  # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
+
+  ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
+  ## are the names of secret variables. They are set in
+  ## GitHub's web interface.
+
+  ## select an entry to build in the following `bundles` set
+  ## defaults to "default"
+  default-bundle = "coq-master";
+
+  ## write one `bundles.name` attribute set per
+  ## alternative configuration
+  ## When generating GitHub Action CI, one workflow file
+  ## will be created per bundle
+  bundles = let
+    ## In some cases, light overrides are not available/enough
+    ## in which case you can use either
+    # coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
+    ## or a "long" overlay to put in `.nix/coq-overlays
+    ## you may use `nix-shell --run fetchOverlay <coq-pkg>`
+    ## to automatically retrieve the one from nixpkgs
+    ## if it exists and is correctly named/located
+
+    ## You can override Coq and other coqPackages
+    ## through the following attribute
+    ## If <ocaml-pkg> does not support light overrides,
+    ## you may use `overrideAttrs` or long overlays
+    ## located in `.nix/ocaml-overlays`
+    ## (there is no automation for this one)
+    #  ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
+
+    ## You can also override packages from the nixpkgs toplevel
+    # <nix-pkg>.override.overrideAttrs = o: <overrides>;
+    ## Or put an overlay in `.nix/overlays`
+
+    ## you may mark a package as a main CI job (one to take deps and
+    ## rev deps from) as follows
+    # coqPackages.<main-pkg>.main-job = true;
+    ## by default the current package and its shell attributes are main jobs
+
+    ## you may mark a package as a CI job as follows
+    #  coqPackages.<another-pkg>.job = "test";
+    ## It can then built through
+    ## nix-build --argstr bundle "default" --arg job "test";
+    ## in the absence of such a directive, the job "another-pkg" will
+    ## is still available, but will be automatically included in the CI
+    ## via the command genNixActions only if it is a dependency or a
+    ## reverse dependency of a job flagged as "main-job" (see above).
+
+    ## Run on push on following branches (default [ "master" ])
+    # push-branches = [ "master" "branch2" ];
+
+    master = [
+      "stdlib"
+      "mathcomp"
+      "fourcolor"
+      "odd-order"
+      "mathcomp-zify"
+      "mathcomp-finmap"
+      "mathcomp-bigenough"
+      "mathcomp-analysis"
+      # TODO unimath
+      # TODO unicoq
+      # "math-classes" -> overlay
+      # "corn" -> overlay
+      "stdpp"
+      "iris"
+      # "autosubst" -> overlay
+      # TODO tests from iris/examples
+      # TODO hott
+      # "coqhammer" -> overlay
+      # "flocq" -> overlay
+      # TODO coq-performance-tests
+      # TODO coq-tools
+      "coquelicot"
+      # "compcert" -> overlay
+      "vst"
+      # TODO cross-crypto
+      # TODO rewriter
+      # TODO fiat_parsers
+      # TODO fiat_crypto_legacy
+      # TODO fiat_crypto
+      # TODO rupicola
+      # TODO bedrock2
+      # TODO coqutil
+      # TODO kami
+      # TODO riscv_coq
+      # TODO color
+      "bignums"
+      "coqprime"
+      # TODO bbv
+      # TODO coinduction
+      # "coq-elpi" -> overlay
+      "hierarchy-builder"
+      # TODO engine bench
+      # TODO fcsl_pcm
+      # "coq-ext-lib" -> overlay
+      # "simple-io" -> overlay
+      # "QuickChick" -> overlay
+      # TODO reduction_effects
+      # TODO menhirlib
+      # TODO neural_net_interp
+      # "aac-tactics" -> overlay
+      "paco"
+      # TODO itree
+      # TODO itree_io
+      "ceres"
+      "parsec"
+      # TODO json
+      # TODO async_test
+      # TODO http
+      "paramcoq"
+      # "relation-algebra" -> overlay
+      "StructTact"
+      "InfSeqExt"
+      "Cheerios"
+      "Verdi"
+      # TODO verdi-raft
+      # TODO stdlib2
+      # TODO argosy
+      # TODO atbr
+      # TODO perennial
+      # TODO sf
+      # TODO Coqtail
+      "deriving"
+      # TODO vscoq (is vscoq-language-server enough?)
+      # "category-theory" -> overlay
+      "itauto"
+      # TODO jasmin
+      # TODO coq-lean-importer
+      # TODO smtcoq_trakt
+      # TODO stalmarck
+      # TODO tactician
+      # TODO ltac2_compiler
+      # TODO waterproof
+      # TODO autosubst OCaml
+    ];
+    coq-master = [
+      "dpdgraph"
+      "smtcoq"
+      "trakt"
+    ];
+    main = [
+      "coq-lsp"
+      # "equations" -> overlay
+      # "metacoq" -> overlay
+      "serapi"
+      "mathcomp-word"
+    ];
+    common-bundles = listToAttrs (forEach master (p:
+      { name = p; value.override.version = "master"; }))
+    // listToAttrs (forEach coq-master (p:
+      { name = p; value.override.version = "coq-master"; }))
+    // listToAttrs (forEach main (p:
+      { name = p; value.override.version = "main"; }))
+    // {
+      coq-elpi.override.version = "proux01:split_stdlib";
+      mathcomp.override.version = "proux01:split_stdlib";
+      # tlc.override.version = "master-for-coq-ci"; -> overlay
+      tlc.override.version = "proux01:split_stdlib";
+      flocq.override.version = "split_stdlib";
+      coq-ext-lib.override.version = "split_stdlib";
+      aac-tactics.override.version = "split_stdlib";
+      coqhammer.override.version = "proux01:split_stdlib";
+      math-classes.override.version = "split_stdlib";
+      corn.override.version = "split_stdlib";
+      equations.override.version = "proux01:split_stdlib";
+      autosubst.override.version = "split_stdlib";
+      relation-algebra.override.version = "proux01:split_stdlib";
+      category-theory.override.version = "proux01:split_stdlib";
+      metacoq.override.version = "proux01:split_stdlib";
+      compcert.override.version = "proux01:split_stdlib";
+      simple-io.override.version = "proux01:split_stdlib";
+      QuickChick.override.version = "proux01:split_stdlib";
+    };
+  in {
+    "coq-master".coqPackages = common-bundles // {
+      coq.override.version = "proux01:split_stdlib";
+    };
+    "coq-master".ocamlPackages = { elpi.override.version = "1.19.2"; };
+  };
+}

.nix/coq-nix-toolbox.nix

@@ -0,0 +1 @@
+"3170ff10f08b5767b9763c05e71d7481b5fdcc30"

.nix/coq-overlays/QuickChick/default.nix

@@ -0,0 +1,67 @@
+{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io, version ? null }:
+
+let recent = lib.versions.isGe "8.7" coq.coq-version || coq.coq-version == "dev"; in
+(mkCoqDerivation {
+  pname = "QuickChick";
+  owner = "QuickChick";
+  inherit version;
+  defaultVersion = with lib; with versions; lib.switch [ coq.coq-version ssreflect.version ] [
+      { cases = [ (range "8.15" "8.19") pred.true  ]; out = "2.0.2"; }
+      { cases = [ (range "8.13" "8.17") pred.true  ]; out = "1.6.5"; }
+      { cases = [ "8.13" pred.true  ]; out = "1.5.0"; }
+      { cases = [ "8.12" pred.true  ]; out = "1.4.0"; }
+      { cases = [ "8.11" pred.true  ]; out = "1.3.2"; }
+      { cases = [ "8.10" pred.true  ]; out = "1.2.1"; }
+      { cases = [ "8.9"  pred.true  ];  out = "1.1.0"; }
+      { cases = [ "8.8"  pred.true  ];  out = "20190311"; }
+      { cases = [ "8.7"  isLe "1.8" ];  out = "1.0.0"; }
+      { cases = [ "8.6"  pred.true  ];  out = "20171102"; }
+      { cases = [ "8.5"  pred.true  ];  out = "20170512"; }
+    ] null;
+  release."2.0.2".sha256    = "sha256-xxKkwDRjB8nUiXNhein1Ppn0DP5FZ13J90xUPAnQBbs=";
+  release."2.0.1".sha256    = "sha256-gJc+9Or6tbqE00920Il4pnEvokRoiADX6CxP/Q0QZaY=";
+  release."1.6.5".sha256    = "sha256-rcFyRDH8UbB9KVk10P5qjtPkWs04p78VNHkCq4mXr3U=";
+  release."1.6.4".sha256    = "sha256-C1060wPSU33yZAFLxGmZlAMXASnx98qz3oSLO8DO+mM=";
+  release."1.6.2".sha256    = "0g5q9zw3xd4zndihq96nxkq4w3dh05418wzlwdk1nnn3b6vbx6z0";
+  release."1.5.0".sha256    = "1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dcw7hyfkw";
+  release."1.4.0".sha256    = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc";
+  release."1.3.2".sha256    = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs";
+  release."1.2.1".sha256    = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46";
+  release."1.1.0".sha256    = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3";
+  release."1.0.0".sha256    = "1gqy9a4yavd0sa7kgysf9gf2lq4p8dmn4h89y8081f2j8zli0w5y";
+  release."20190311".rev    = "22af9e9a223d0038f05638654422e637e863b355";
+  release."20190311".sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq";
+  release."20171102".rev    = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf";
+  release."20171102".sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17";
+  release."20170512".rev    = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03";
+  release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg";
+  releaseRev = v: "v${v}";
+
+  preConfigure = lib.optionalString recent
+    "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
+
+  useDuneifVersion = v: lib.versions.isGe "2.1" v || v == "dev";
+  opam-name = "coq-quickchick";
+
+  mlPlugin = true;
+  nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
+  propagatedBuildInputs = [ ssreflect ]
+    ++ lib.optionals recent [ coq-ext-lib simple-io ];
+  extraInstallFlags = [ "-f Makefile.coq" ];
+
+  enableParallelBuilding = false;
+
+  meta = with lib; {
+    description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck";
+    maintainers = with maintainers; [ jwiegley ];
+  };
+}).overrideAttrs (o:
+  let after_1_6 = lib.versions.isGe "1.6" o.version || o.version == "dev";
+      after_2_1 = lib.versions.isGe "2.1" o.version || o.version == "dev";
+  in {
+    nativeBuildInputs = o.nativeBuildInputs
+    ++ lib.optional after_1_6 coq.ocamlPackages.cppo
+    ++ lib.optional after_2_1 coq.ocamlPackages.menhir;
+    propagatedBuildInputs = o.propagatedBuildInputs
+    ++ lib.optionals after_1_6 (with coq.ocamlPackages; [ findlib zarith ]);
+})