Re-enable Alectryon with vsrocqtop

Author: shilangyu

.github/pip-requirements.txt

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

.github/workflows/ci.yml

@@ -64,6 +64,8 @@ jobs:
               echo "::group::Install opam packages"
               opam pin add -n -k version coq ${{ matrix.rocq }}
               opam install --confirm-level=unsafe-yes --deps-only .
+              # vsrocqtop is needed by Alectryon
+              opam install --confirm-level=unsafe-yes vsrocq-language-server
               echo "::endgroup::"
 
               echo "::group::Print opam config (post-install)"

README.md

@@ -37,6 +37,13 @@ The mechanization has the following properties:
     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 [vsrocqtop](https://github.com/rocq-prover/vsrocq).
+    ```
+    opam install vsrocq-language-server
+    ```
+
 Alternatively, a [nix](https://nixos.org/) flake installing all the dependencies is provided:
 ```
 nix develop
@@ -48,7 +55,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/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.
+- `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. Alternatively, if you installed Alectryon, you can open the generated [webpage](_build/default/examples/rocq_proof/Example.html) in your web browser.
 
 ## Structure of the repository
 

examples/rocq_proof/dune

@@ -1,14 +1,13 @@
-; LATER: re-enable when Alectryon supports Rocq 9.0
-; (rule
-;  (target Example.html)
-;  (deps (package warblre) (:input (file Example.v)))
-;  (action
-;   (run alectryon -Q ../../mechanization Warblre --long-line-threshold -1 %{input}))
-;  (enabled_if %{bin-available:alectryon}))
+(rule
+ (target Example.html)
+ (deps (package warblre) (:input (file Example.v)))
+ (action
+  (run alectryon --coq-driver vsrocq -Q ../../mechanization Warblre --long-line-threshold -1 %{input}))
+ (enabled_if %{bin-available:alectryon}))
 
-; (rule
-;  (target dummy)
-;  (action (progn
-;   (echo "Alectryon not installed: skipping examples/rocq_proof\n")
-;   (write-file dummy "")))
-;  (enabled_if (not %{bin-available:alectryon})))
+(rule
+ (target dummy)
+ (action (progn
+  (echo "Alectryon not installed: skipping examples/rocq_proof\n")
+  (write-file dummy "")))
+ (enabled_if (not %{bin-available:alectryon})))

specification_check/rocq_parser.py

@@ -4,7 +4,7 @@
 from dataclasses import dataclass
 from typing import Dict, List, Tuple
 
-from alectryon.literate import Comment, StringView, coq_partition
+from alectryon.literate import Comment, StringView, CoqParser
 from spec_merger.aligner_utils import Position
 from spec_merger.content_classes.dictionary import Dictionary
 from spec_merger.content_classes.string import String
@@ -96,7 +96,7 @@ def __process_lines(self, rocq_code, all_filenames, matcher: re.Pattern) -> list
         comments = []
         for filename in all_filenames:
             file = rocq_code[filename]
-            partition = coq_partition(file)
+            partition = CoqParser(file).partition()
             for field in partition:
                 if isinstance(field, Comment) and matcher.match(str(field.v)):
                     start_line_num = ROCQParser.__get_line_num(field.v)