Merge branch 'rocq-prover:master' into refactor-vector

Author: andres-erbsen

.github/workflows/alpine.yml

@@ -35,7 +35,17 @@ jobs:
       with:
         branch: ${{ matrix.alpine }}
         extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing
-        packages: rocq dune
-    - name: dune build -p rocq-stdlib
+        packages: rocq dune  bash python3 graphviz  make findutils diffutils grep rsync
+    - name: 'dune build @stdlib-html # depends on stdlib'
       shell: alpine.sh {0}
-      run: dune build -p rocq-stdlib
+      run: 'dune build @stdlib-html # depends on stdlib'
+    - name: 'find _build/default/doc/stdlib/html/ -iname "*\**" -print -delete # for upload-artifact'
+      shell: alpine.sh {0}
+      run: 'find _build/default/doc/stdlib/html/ -iname "*\**" -print -delete # for upload-artifact'
+    - uses: actions/upload-artifact@v4
+      with:
+        name: stdlib-html
+        path: _build/default/doc/stdlib/html
+    - name: Check for duplicate files
+      shell: alpine.sh {0}
+      run: dev/tools/check-duplicate-files.sh

.github/workflows/basic-checks.yml

@@ -157,12 +157,14 @@ bin
 # generated by dune build -p
 *.install
 
+# generated by /theories/All.sh in make-based build
+/theories/All.v
+
 .dune-stamp
 theories/dune
 user-contrib/Ltac2/dune
 /test-suite/test_suite_config.inc
 
 .wrappers
-rocq-stdlib-doc.opam
 doc/stdlib/Library.fdb_latexmk
 doc/stdlib/Library.fls

.github/workflows/nix-action-rocq-9.0.yml .github/workflows/nix-action-rocq-9.1.yml.github/workflows/nix-action-rocq-9.0.yml renamed to .github/workflows/nix-action-rocq-9.1.yml

@@ -35,25 +35,25 @@ with builtins; with (import <nixpkgs> {}).lib;
   # 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";
   cachix.coq.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 = "rocq-9.0";
+  default-bundle = "rocq-9.1";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
@@ -116,7 +116,6 @@ with builtins; with (import <nixpkgs> {}).lib;
       "coqprime"
       "coquelicot"
       "coqutil"
-      "coq-elpi"
       "ExtLib"
       "coq-hammer"
       "coq-hammer-tactics"
@@ -145,12 +144,14 @@ with builtins; with (import <nixpkgs> {}).lib;
       "mathcomp-algebra"
       "mathcomp-algebra-tactics"
       "mathcomp-analysis"
+      "mathcomp-boot"
       "mathcomp-bigenough"
       "mathcomp-character"
       "mathcomp-classical"
       "mathcomp-field"
       "mathcomp-fingroup"
       "mathcomp-finmap"
+      "mathcomp-order"
       "mathcomp-reals"
       "mathcomp-solvable"
       "mathcomp-ssreflect"
@@ -162,12 +163,12 @@ with builtins; with (import <nixpkgs> {}).lib;
       "paco"
       "paramcoq-test"
       "parsec"
-      "perennial"
       "QuickChick"
       "quickchick-test"
       "relation-algebra"
       "rewriter"
       "riscvcoq"
+      "rocq-lean-import"
       "rupicola"
       "sf"
       "simple-io"
@@ -177,7 +178,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       "unicoq"
       "Verdi"
       "VerdiRaft"
-      "vst"
+      "VST"
     ];
     coq-master = [
       "dpdgraph-test"
@@ -193,74 +194,165 @@ with builtins; with (import <nixpkgs> {}).lib;
       "metarocq"
       "metarocq-test"
     ];
+    # To lighten the CI on released version, don't test reverse dependencies
+    # of Stdlib that take >= 5 min of CI (and their reverse dependencies)
+    lighten-released = [
+      "bedrock2"
+      "category-theory"
+      "CoLoR"
+      "coq-performance-tests"
+      "coq-tools"
+      "corn"
+      "cross-crypto"
+      "engine-bench"
+      "fiat-crypto"
+      "fiat-crypto-ocaml"
+      "iris"
+      "iris-examples"
+      "metacoq"
+      "metacoq-common"
+      "metacoq-erasure"
+      "metacoq-erasure-plugin"
+      "metacoq-pcuic"
+      "metacoq-quotation"
+      "metacoq-safechecker"
+      "metacoq-safechecker-plugin"
+      "metacoq-template-coq"
+      "metacoq-template-pcuic"
+      "metacoq-translations"
+      "metacoq-utils"
+      "metarocq"
+      "metarocq-erasure"
+      "metarocq-erasure-plugin"
+      "metarocq-pcuic"
+      "metarocq-quotation"
+      "metarocq-safechecker"
+      "metarocq-safechecker-plugin"
+      "metarocq-template-pcuic"
+      "metarocq-test"
+      "rewriter"
+      "riscvcoq"
+      "rupicola"
+      "VerdiRaft"
+    ];
     coq-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.elpi-version = "2.0.7";
-      fiat-crypto-legacy.override.version = "sp2019latest";
+      coq-elpi.override.version = "master";
+      coq-elpi.override.elpi-version = "3.4.2";
       tlc.override.version = "master-for-coq-ci";
       smtcoq-trakt.override.version = "with-trakt-coq-master";
       coq-tools.override.version = "proux01:coq_19955";
       stdlib-refman-html.job = true;
+      iris-examples.job = false;  # Currently broken
       jasmin.job = false;  # Currently broken, c.f., https://github.com/rocq-prover/rocq/pull/20589
+      ElmExtraction.job = false;  # not in Rocq CI
+      RustExtraction.job = false;  # not in Rocq CI
+      interval.job = false;  # not in Rocq CI
+      parseque.job = false;  # not in Rocq CI
+      LibHyps.job = false;  # not in Rocq CI
       # To add a simple overlay applying to all bundles,
-      # add below a line like
+      # add, just below this comment, a line like
       #<package>.override.version = "<github_login>:<branch>";
       # where
       # * <package> will typically be one of the strings above (without the quotes)
       #   or look at https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules
       #   for a complete list of Coq packages available in Nix
       # * <github_login>:<branch> is such that this will use the branch <branch>
       #   from https://github.com/<github_login>/<repository>
+      sf.job = false;  # temporarily disactivated in Rocq CI
+      trakt.job = false;  # temporarily disactivated in Rocq CI
+      smtcoq-trakt.job = false;  # temporarily disactivated in Rocq CI
     };
     common-bundles = {
       bignums.override.version = "master";
       rocq-elpi.override.version = "master";
-      rocq-elpi.override.elpi-version = "2.0.7";
+      rocq-elpi.override.elpi-version = "3.4.2";
       rocq-elpi-test.override.version = "master";
-      stdlib-html.job = true;
-      stdlib-test.job = true;
-      stdlib-subcomponents.job = true;
+      hierarchy-builder.override.version = "master";
     };
   in {
     "rocq-master" = { rocqPackages = common-bundles // {
       rocq-core.override.version = "master";
+      stdlib-test.job = true;
     }; coqPackages = coq-common-bundles // {
       coq.override.version = "master";
     }; };
-    "rocq-9.0" = { rocqPackages = common-bundles // {
-      rocq-core.override.version = "9.0.0";
+    "rocq-9.2" = { rocqPackages = common-bundles // {
+      rocq-core.override.version = "9.2";
+      # check that we compile without warnings on last release of Rocq
+      stdlib-warnings.job = true;
+      # plugin pins, from v9.2 branch of Rocq
+      bignums.override.version = "30a45625546da0a88db8689a8009d580aa3f557f";
+      stdlib-test.job = false;
     }; coqPackages = coq-common-bundles // {
-      coq.override.version = "9.0.0";
-      # plugin pins, from v9.0 branch of Coq
-      aac-tactics.override.version = "109af844f39bf541823271e45e42e40069f3c2c4";
+      coq.override.version = "9.2";
+      # plugin pins, from v9.2 branch of Rocq
+      aac-tactics.override.version = "4f796a7b0ee88330162727fc6ea988a7e0ea46e3";
       atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543";
-      itauto.override.version = "c13c6b4a0070ecc3ae8ea9755a1d6a163d123127";
-      bignums.override.version = "cc2d9ee990e4cfebe5f107d8357198baa526eded";
-      coinduction.override.version = "09caaf1f809e3e91ebba05bc38cef6de83ede3b3";
-      dpdgraph-test.override.version = "74ced1b11a8df8d4c04c3829fcf273aa63d2c493";
-      coq-hammer.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
-      coq-hammer-tactics.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
-      equations.override.version = "1.3.1+9.0";
+      bignums.override.version = "30a45625546da0a88db8689a8009d580aa3f557f";
+      itauto.job = false;  # broken
+      coinduction.override.version = "9502ae09e9f87518330f37c08bc19a8c452dcd91";
+      dpdgraph-test.override.version = "7a0fba21287dd8889c55e6611f8ba219d012b81b";
+      coq-hammer.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
+      coq-hammer-tactics.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
+      equations.override.version = "757662b9c875d7169a07b861d48e82157520ab1a";
       equations-test.job = false;
       fiat-parsers.job = false;  # broken
-      metarocq.override.version = "1.4-9.0";
-      metarocq-test.override.version = "v1.4-9.0";
-      mtac2.override.version = "1cdb2cb628444ffe9abc6535f6d2e11004de7fc1";
-      paramcoq-test.override.version = "32609ca4a9bf4a0e456a855ea5118d8c00cda6be";
-      perennial.job = false;  # broken
-      relation-algebra.override.version = "7966d1a7bb524444120c56c3474717bcc91a5215";
-      rewriter.override.version = "30c8507c1e30626b2aa1e15c0aa7c23913da033c";
+      metarocq.override.version = "e8f8078e756cc378b830eb5a8e4637df43d481af";
+      metarocq-test.override.version = "e8f8078e756cc378b830eb5a8e4637df43d481af";
+      mtac2.override.version = "fe8b6049835caa793436e277a64ee7e4910f7b04";
+      paramcoq-test.override.version = "f8026210f37faf6c4031de24ada9fdded29d67e5";
+      relation-algebra.override.version = "ba3db5783060d9e25d1db5e377fc9d71338a5160";
+      rewriter.override.version = "dd37fb28ed7f01a3b7edc0675a86b95dd3eb1545";
+      rocq-lean-import.override.version = "b8291b9dae4f5ed780112e95eea484e435199b46";
+      smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf";
+      # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
+      stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
+      unicoq.override.version = "d52374ca86e3885197f114555e742420fa9bbe94";
+      waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a";
+      compcert.job = false;  # broken
+      VST.job = false;  # depends on compcert
+    } // listToAttrs (forEach lighten-released (p:
+      { name = p; value.job = false; })); };
+    "rocq-9.1" = { rocqPackages = common-bundles // {
+      rocq-core.override.version = "9.1";
+      # plugin pins, from v9.1 branch of Rocq
+      bignums.override.version = "9f9855536bd4167af6986f826819e32354b7da22";
+      stdlib-test.job = false;
+    }; coqPackages = coq-common-bundles // {
+      coq.override.version = "9.1";
+      # plugin pins, from v9.1 branch of Rocq
+      aac-tactics.override.version = "e68d028cef838f5821d184fed0caea9eedd5538a";
+      atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543";
+      bignums.override.version = "9f9855536bd4167af6986f826819e32354b7da22";
+      itauto.job = false;  # broken
+      coinduction.override.version = "823b424778feff8fbd9759bc3a044435ea4902d1";
+      dpdgraph-test.override.version = "7817def06d4e3abc2e54a2600cf6e29d63d58b8a";
+      coq-hammer.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
+      coq-hammer-tactics.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
+      equations.override.version = "2137c8e7081f2d47ab903de0cc09fd6a05bfab01";
+      equations-test.job = false;
+      fiat-parsers.job = false;  # broken
+      metarocq.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
+      metarocq-test.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
+      mtac2.override.version = "bcbefa79406fc113f878eb5f89758de241d81433";
+      paramcoq-test.override.version = "937537d416bc5f7b81937d4223d7783d0e687239";
+      relation-algebra.override.version = "4db15229396abfd8913685be5ffda4f0fdb593d9";
+      rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc";
+      rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444";
       smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
-      smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
+      # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
       stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
-      unicoq.override.version = "a9b72f755539c0b3280e38e778a09e2b7519a51a";
-      waterproof.override.version = "443f794ddc102309d00f1d512ab50b84fdc261aa";
+      unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1";
+      waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a";
       compcert.job = false;  # broken
-    }; };
+      VST.job = false;  # depends on compcert
+    } // listToAttrs (forEach lighten-released (p:
+      { name = p; value.job = false; })); };
   };
 }

.github/workflows/nix-action-rocq-9.2.yml

@@ -1 +1 @@
-"52aaa743836510268bf94deb898de0f8bd0501be"
+"60810ce1d3e73bece989ce9b9c42d9452c1d54a5"