Rocq 9.0.0

.github/pip-requirements.txt

@@ -1,4 +1,4 @@
-alectryon == 1.4.0
+alectryon @ git+https://github.com/cpitclaudel/alectryon@a02a99c75c4166efc8812a600e8cbf4588424c0f
 git+https://github.com/epfl-systemf/SpecMerger
-requests == 2.32.3
+requests == 2.32.4
 beautifulsoup4 == 4.12.3

.github/workflows/ci.yml

@@ -14,15 +14,15 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        coq: [ "8.18.0", "8.19.2" ]
-        node: [ "21.7.2", "22.4.1" ]
+        rocq: [ "9.0.0", "9.1.0" ]
+        node: [ "24.13.0" ]
       fail-fast: false
     steps:
       - name: Checkout repository
-        uses: actions/checkout@v4
+        uses: actions/checkout@v6
 
       - name: Install Node.js
-        uses: actions/setup-node@v4
+        uses: actions/setup-node@v6
         with:
           node-version: ${{ matrix.node }}
           cache: 'npm'
@@ -51,9 +51,9 @@ jobs:
         uses: actions/cache@v4
         with:
           path: /home/runner/work/Warblre/Warblre/_opam
-          key: opam-packages-cache-${{runner.os}}-coq${{matrix.coq}}-${{ hashFiles('**/*.opam') }}
+          key: opam-packages-cache-${{runner.os}}-rocq${{matrix.rocq}}-${{ hashFiles('**/*.opam') }}
           restore-keys: |
-                        opam-packages-cache-${{runner.os}}-coq${{matrix.coq}}
+                        opam-packages-cache-${{runner.os}}-rocq${{matrix.rocq}}
                         opam-packages-cache-${{runner.os}}
       - name: Install opam dependencies
         run:  |
@@ -62,10 +62,8 @@ jobs:
               echo "::endgroup::"
 
               echo "::group::Install opam packages"
-              opam pin add -n -k version coq ${{ matrix.coq }}
-              # coq-serapi's dependencies are installed now to ensure
-              opam install --confirm-level=unsafe-yes --deps-only . coq-serapi
-              opam install --confirm-level=unsafe-yes coq-serapi
+              opam pin add -n -k version coq ${{ matrix.rocq }}
+              opam install --confirm-level=unsafe-yes --deps-only .
               echo "::endgroup::"
 
               echo "::group::Print opam config (post-install)"
@@ -80,10 +78,10 @@ jobs:
         run:  |
               opam exec -- dune test --force --display=verbose
 
-      - name: Check compiled libraries (coqchk)
+      - name: Check compiled libraries (rocqchk)
         run:  |
               ALL_VOS=$(find _build/default/mechanization/ -name '*.vo');
-              opam exec -- coqchk -silent --output-context -Q _build/default/mechanization Warblre $ALL_VOS
+              opam exec -- rocqchk -silent --output-context -Q _build/default/mechanization Warblre $ALL_VOS
 
       - name: Test install of Warblre
         run:  |

.gitignore

@@ -1,10 +1,16 @@
-# Coq(ide) generated files
+# Rocq/CoqIDE generated files
 .lia.cache
 \#*\#
 
+# This file gets generated by dune, and contains install-dependent paths
+_RocqProject
+
 # Dune's build directory
 _build/
 
+# Opam's directory
+_opam/
+
 # VsCode's configuration
 .vscode/
 
@@ -16,4 +22,4 @@ _build/
 node_modules
 
 # python
-*/__pycache__
+*/__pycache__

.nix/dune.nix

@@ -0,0 +1,57 @@
+# Based on
+# https://github.com/NixOS/nixpkgs/blob/2375cc015c9c2d5dfaff876d063cd9218ae89a84/pkgs/development/tools/ocaml/dune/3.nix
+
+{
+  lib,
+  stdenv,
+  fetchurl,
+  ocaml,
+  findlib,
+  ocaml-lsp,
+  dune-release,
+  fetchFromGitHub,
+}:
+
+stdenv.mkDerivation rec {
+  pname = "dune";
+  version = "3.21.0";
+
+  src = fetchFromGitHub {
+    owner = "ocaml";
+    repo = "dune";
+    rev = "6e9d965bb5bbadfe9cbf89314cb6f8ecaa845bd9";
+    hash = "sha256-YOey/GwrJVrQwEgoV8taDF6t6LgCJtrtmPQPvAtA7EQ=";
+  };
+
+  nativeBuildInputs = [
+    ocaml
+    findlib
+  ];
+
+  strictDeps = true;
+
+  buildFlags = [ "release" ];
+
+  dontAddPrefix = true;
+  dontAddStaticConfigureFlags = true;
+  configurePlatforms = [ ];
+
+  installFlags = [
+    "PREFIX=${placeholder "out"}"
+    "LIBDIR=$(OCAMLFIND_DESTDIR)"
+  ];
+
+  passthru.tests = {
+    inherit ocaml-lsp dune-release;
+  };
+
+  meta = {
+    homepage = "https://dune.build/";
+    description = "Composable build system";
+    mainProgram = "dune";
+    changelog = "https://github.com/ocaml/dune/raw/${version}/CHANGES.md";
+    maintainers = [ lib.maintainers.vbgl ];
+    license = lib.licenses.mit;
+    inherit (ocaml.meta) platforms;
+  };
+}

.nix/vsrocq-language-server.nix

@@ -0,0 +1,65 @@
+# Based on
+# https://github.com/NixOS/nixpkgs/blob/nixos-25.11/pkgs/development/rocq-modules/vsrocq-language-server/default.nix
+
+{
+  metaFetch,
+  coq_9_1,
+  rocq-core_9_1,
+  lib,
+  glib,
+  adwaita-icon-theme,
+  wrapGAppsHook3,
+  fetchFromGitHub,
+}:
+
+let
+  ocamlPackages = rocq-core_9_1.ocamlPackages;
+
+  repo = fetchFromGitHub {
+    owner = "rocq-prover";
+    repo = "vsrocq";
+    rev = "v2.3.4";
+    hash = "sha256-v1hQjE8U1o2VYOlUjH0seIsNG+NrMNZ8ixt4bQNyGvI=";
+  };
+in
+ocamlPackages.buildDunePackage {
+  pname = "vsrocq-language-server";
+  version = "2.3.4";
+  src = "${repo}/language-server";
+  nativeBuildInputs = [ coq_9_1 ];
+  buildInputs = [
+    coq_9_1
+    glib
+    adwaita-icon-theme
+    wrapGAppsHook3
+  ]
+  ++ (with ocamlPackages; [
+    findlib
+    lablgtk3-sourceview3
+    zarith
+    ppx_inline_test
+    ppx_assert
+    ppx_sexp_conv
+    ppx_deriving
+    ppx_import
+    sexplib
+    (ppx_yojson_conv.override {
+      ppx_yojson_conv_lib = ppx_yojson_conv_lib.override { yojson = yojson_2; };
+    })
+    lsp
+    sel
+    ppx_optcomp
+  ]);
+  preBuild = ''
+    make dune-files
+  '';
+
+  meta =
+    with lib;
+    {
+      description = "Language server for the vsrocq vscode/codium extension";
+      homepage = "https://github.com/rocq-prover/vsrocq";
+      maintainers = with maintainers; [ cohencyril ];
+      license = licenses.mit;
+    };
+}

README.md

@@ -1,6 +1,6 @@
-# Warblre: A Coq mechanization of ECMAScript regexes
+# Warblre: A Rocq mechanization of ECMAScript regexes
 
-This repository contains *Warblre*, a Coq mechanization of ECMAScript regexes.
+This repository contains *Warblre*, a Rocq mechanization of ECMAScript regexes.
 [ECMAScript](https://ecma-international.org/publications-and-standards/standards/ecma-262/) is the specification followed by JavaScript implementations, and a mechanization of its regex semantics makes it possible to reason formally about these regexes from a proof assistant.
 
 The mechanization has the following properties:
@@ -26,23 +26,17 @@ The mechanization has the following properties:
     ```shell
     opam install . --deps-only
     ```
-    This will allow you to step through the Coq code, extract the OCaml code and compile it.
+    This will allow you to step through the Rocq code, extract the OCaml code and compile it.
 2. **[Optional]**  
     In order to pack and and run the JavaScript code, you will need to install [Node.js](https://nodejs.org/en), e.g. using [nvm](https://github.com/nvm-sh/nvm).
     ```shell
-    nvm install 21.7.2
+    nvm install 24.13.0
     ```
     as well as some JavaScript dependencies:
     ```shell
     npm install # Install packages used by our JavaScript code
     npm install -g webpack-cli # Install webpack-cli, which is used to pack the code in monolithic JavaScript files
     ```
-3. **[Optional]**  
-    [Alectryon](https://github.com/cpitclaudel/alectryon) is used to produced literate examples.
-    You will also need [serapi](https://github.com/ejgallego/coq-serapi).
-    ```
-    opam install coq-serapi
-    ```
 
 Alternatively, a [nix](https://nixos.org/) flake installing all the dependencies is provided:
 ```
@@ -55,7 +49,7 @@ npm install
 - `dune exec example` will run an example of matching a string with a regex ([source](examples/ocaml_example/Main.ml)).
 - **[Requires JavaScript dependencies]**  
     `dune exec fuzzer` will build and run the fuzzer to compare the extracted engine against Irregexp (Node.js's regex engine).
-- `dune build examples/coq_proof` will build everything so that you can step through [examples/coq-proof/Example.v](examples/coq_proof/Example.v), which demonstrates how Warblre can be used to reason about JavaScript regexes. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/coq_proof/Example.html) in your web browser.
+- `dune build examples/rocq_proof` will build everything so that you can step through [examples/rocq-proof/Example.v](examples/rocq_proof/Example.v), which demonstrates how Warblre can be used to reason about JavaScript regexes.
 
 ## Structure of the repository
 
@@ -76,15 +70,15 @@ The repository is structured as follows:
 ├── examples
 │   ├── browser_playground
 │   ├── cmd_playground
-│   ├── coq_proof
+│   ├── rocq_proof
 │   └── ocaml_example
 └── tests
     ├── tests
     ├── fuzzer
     └── test262
 ```
 
-- **[Mechanization](#mechanization)**: Warblre proper, the mechanization in Coq of the ECMASCript semantics of regexes.
+- **[Mechanization](#mechanization)**: Warblre proper, the mechanization in Rocq of the ECMASCript semantics of regexes.
 - **[Engines](#engines)**: Extraction directives and extra code to allow a smooth usage of the extracted engine in different programming languages. Most of the code is in `common`; the other directories contain code specific to one particular language.
 - **Examples**: Code snippets which show how to use the mechanization and extracted engines.
 - **Tests:**
@@ -96,7 +90,7 @@ The follow subsections further detail some of these.
 
 ## Mechanization
 
-The `mechanization` directory contains the Coq code mechanizing the subset of the ECMAScript specification which describes regexes and their semantics.
+The `mechanization` directory contains the Rocq code mechanizing the subset of the ECMAScript specification which describes regexes and their semantics.
 It is based on the 14th edition from June 2023, available [here](https://262.ecma-international.org/14.0/).
 Regexes are described in chapter [22.2](https://tc39.es/ecma262/2023/multipage/text-processing.html#sec-regexp-regular-expression-objects).
 
@@ -115,7 +109,7 @@ The mechanization depends on external types and parameters (for instance for uni
 This is encoded with a functor, whose parameter is described in `mechanization/spec/API.v`.
 
 Files are organized as follows:
-- **spec**: the mechanization in itself, translating the paper specification into Coq.
+- **spec**: the mechanization in itself, translating the paper specification into Rocq.
 - **props**: proofs about the specification. The main proofs are
     - *Compilation failure-free*: if a regex is early-errors-free, then its compilation into a matcher does not raise an error.
     - *Matching failure-free*: if a matcher is provided with valid inputs, then the matching process does not raise an error.

doc/Differences.md

@@ -110,15 +110,15 @@ The specification contains a few assertions which ensure that numbers can be saf
 >
 >> Assert: n < 2^32 - 1.
 
-These checks are currently not mechanized, as unbound integers are used in Coq, OCaml and JavaScript.
+These checks are currently not mechanized, as unbound integers are used in Rocq, OCaml and JavaScript.
 
 ## Non-structurally recursive functions
 
 Some functions in the specification, `RepeatMatcher` being the the most infamous one, are generally recursive.
-Such definitions would be rejected by Coq, as it cannot syntactically ensure their termination.
+Such definitions would be rejected by Rocq, as it cannot syntactically ensure their termination.
 
 We modified such definitions into fuel-based functions.
-This transformation allows Coq to ensure their termination,
+This transformation allows Rocq to ensure their termination,
 since the function is then structurally recursive on the fuel (which is represented using a `nat`).
 
 Intuitively, the equivalence of the two functions (before and after transformation) relies on being able to compute a sufficient amount of fuel **prior** to the first call, and on the fact that such a fuel amount exists to begin with.
@@ -200,11 +200,14 @@ Some of these other functions were mechanized (`CodePointAt`, `AdvanceStringInde
 The axiomatization of functions left abstract is *minimal*, in the sense that only axioms which are necessary to ensure the safety and termination of the specification: these functions should most likely satisfy other properties to be considered correct.
 
 > For instance, `canonicalize` has no applicable axiom, which would allow for characters such that
-> ```Coq
+>
+> ```rocq
 > canonicalize c1 = c2 /\ canonicalize c2 = c1
 > ```
+>
 > which would yield some surprising behaviors. In fact, `canonicalize` should most likely be idempotent:
-> ```Coq
+>
+> ```rocq
 > forall c, canonicalize c = canonicalize (canonicalize c)
 > ```