Test against Rocq 9.1.0 in CI.

Signed-off-by: Rodolphe Lepigre <[email protected]>

Author: rlepigre

.github/workflows/workflow.yml

@@ -270,6 +270,26 @@ jobs:
           # We disable the Dune cache when running the tests
           DUNE_CACHE: disabled
 
+  rocq:
+    name: Rocq 9.1.0
+    needs: nix-build
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: nixbuild/nix-quick-install-action@v34
+        with:
+          nix_conf: ${{ env.EXTRA_NIX_CONFIG }}
+      - uses: nix-community/cache-nix-action@v6
+        with:
+          primary-key: |
+            nix-${{ runner.os }}-${{ github.job }}-${{ hashFiles('**/*.nix', '**/flake.lock') }}
+          restore-prefixes-first-match: nix-${{ runner.os }}-${{ github.job }}-
+          gc-max-store-size-linux: 5G
+      - run: nix develop .#rocq -c make test-coq
+        env:
+          # We disable the Dune cache when running the tests
+          DUNE_CACHE: disabled
+
   wasm:
     name: Wasm_of_ocaml
     needs: nix-build

flake.nix

@@ -55,6 +55,14 @@
               ];
             });
           })
+          (self: super: {
+            coq_9_1_native = super.coq_9_1.overrideAttrs (a: {
+              configureFlags = [
+                "-native-compiler"
+                "yes"
+              ];
+            });
+          })
         ];
 
         applyOxcamlPatches = import ./nix/ox-patches.nix {
@@ -353,6 +361,28 @@
               '';
             };
 
+            rocq = pkgs.mkShell {
+              inherit INSIDE_NIX;
+              nativeBuildInputs = (testNativeBuildInputs pkgs);
+              # Coq requires OCaml 4.x
+              inputsFrom = [
+                pkgs.ocaml-ng.ocamlPackages_4_14.dune_3
+              ];
+              buildInputs = with pkgs; [
+                ocaml-ng.ocamlPackages_4_14.csexp
+                ocaml-ng.ocamlPackages_4_14.pp
+                ocaml-ng.ocamlPackages_4_14.re
+                ocaml-ng.ocamlPackages_4_14.spawn
+                ocaml-ng.ocamlPackages_4_14.uutf
+                coq_9_1_native
+                coq_9_1_native.ocamlPackages.findlib
+              ];
+              meta.description = ''
+                Provides a minimal shell environment built purely from nixpkgs
+                that can build Dune and the Rocq testsuite.
+              '';
+            };
+
             bootstrap-check = pkgs.mkShell {
               inherit INSIDE_NIX;
               buildInputs = with pkgs; [