fix and update alectryon

.github/workflows/ci.yml

@@ -159,51 +159,23 @@ jobs:
 # - coqchk: Runs coqchk
 # - install: Tests install target
 
-   # alectryon job
+  # alectryon doc job (using Nix + dune for reproducible builds)
   doc-alectryon:
-    needs: build
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v4
       with:
         submodules: recursive
-    # Download artifact
-    - uses: actions/download-artifact@v4
+    - uses: nixbuild/nix-quick-install-action@v30
+    - uses: nix-community/cache-nix-action@v6
       with:
-        name: workspace-${{ env.coq-version-supported }}
-    # Unpack Tar
-    - run: tar -xf workspace.tar
-    - name: add problem matchers
+        primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }}
+        restore-prefixes-first-match: nix-${{ runner.os }}-
+    - name: Build alectryon docs with dune
       run: |
-        #echo "::add-matcher::etc/coq-scripts/github/coq-oneline-error.json" # now via a script
-        #echo "::add-matcher::etc/coq-scripts/github/coqdoc.json" # disabled for now, since they don't have file names
-        echo "::add-matcher::etc/coq-scripts/github/alectryon-error.json"
-        #echo "::add-matcher::etc/coq-scripts/github/alectryon-warning.json" # too noisy right now, cf https://github.com/cpitclaudel/alectryon/issues/34 and https://github.com/cpitclaudel/alectryon/issues/33
-    - uses: coq-community/[email protected]
-      with:
-        coq_version: ${{ env.coq-version-supported }}
-        ocaml_version: ${{ env.ocaml-version }}
-        custom_script: |
-          opam install -y coq-serapi
-          sudo apt-get -o Acquire::Retries=30 update -q
-          sudo apt-get -o Acquire::Retries=30 install python3-pip python3-venv autoconf -y --allow-unauthenticated
-          startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
-            sudo chown -R 1000:1000 .
-          endGroup
-          # Create and activate a virtual environment
-          python3 -m venv myenv
-          source myenv/bin/activate
-          # Install the required Python packages in the virtual environment
-          python -m pip install --upgrade pip
-          python -m pip install pygments dominate beautifulsoup4 docutils==0.17.1
-          echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
-          make alectryon ALECTRYON_EXTRAFLAGS=--traceback
-    - name: Revert permissions
-      # to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
-      if: ${{ always() }}
-      run: sudo chown -R 1001:116 .
+        nix develop .#coq_9_0 -c dune build @alectryon
     - name: tar alectryon artifact
-      run: tar -cf alectryon-html.tar alectryon-html
+      run: tar -cf alectryon-html.tar -C _build/default alectryon-html
     - name: upload alectryon artifact
       uses: actions/upload-artifact@v4
       with:

.gitmodules

@@ -3,4 +3,4 @@
 	url = https://github.com/JasonGross/coq-scripts.git
 [submodule "etc/alectryon"]
 	path = etc/alectryon
-	url = https://github.com/JasonGross/alectryon.git
+	url = https://github.com/cpitclaudel/alectryon.git

Makefile.coq.local

@@ -172,7 +172,7 @@ alectryon-html/index.html alectryon-html/toc.html alectryon-html/coqdoc.css : al
 
 alectryon-html-done.timestamp: $(ALL_VOFILES) $(ALL_VFILES)
 	@ mkdir -p alectryon-html
-	$(TIMER) $(ALECTRYON) --frontend coq+rst --backend webpage --sertop-arg=--no_prelude --sertop-arg=--indices-matter $(COQLIBS_NOML) --output-directory alectryon-html --cache-directory alectryon-cache --long-line-threshold=99999 $(ALECTRYON_EXTRAFLAGS) $(ALL_VFILES)
+	$(TIMER) $(ALECTRYON) --frontend coq+rst --backend webpage --coq-driver coqlsp --output-directory alectryon-html --cache-directory alectryon-cache --long-line-threshold=99999 $(ALECTRYON_EXTRAFLAGS) $(ALL_VFILES)
 	touch alectryon-html-done.timestamp
 
 alectryon-html:

dune

@@ -48,6 +48,23 @@
   (alias_rec theories/all)
   _CoqProject))
 
+; Alectryon documentation
+; Run with: dune build @alectryon
+
+(rule
+ (target alectryon_rules.sexp)
+ (deps
+  (glob_files theories/*.v)
+  (glob_files theories/**/*.v)
+  (glob_files contrib/*.v))
+ (action
+  (with-stdout-to %{target}
+   (chdir %{project_root}
+    (run etc/gen-alectryon-rules/gen_alectryon_rules.exe)))))
+
+(subdir alectryon-html
+ (dynamic_include ../alectryon_rules.sexp))
+
 ; Tags for emacs
 
 (rule

dune-project

@@ -1,6 +1,7 @@
-(lang dune 3.13)
+(lang dune 3.14)
 
 (using coq 0.8)
+(using directory-targets 0.1)
 
 (name coq-hott)
 

etc/gen-alectryon-rules/README.md

@@ -0,0 +1,68 @@
+# Alectryon Rules Generator
+
+This tool generates dune rules for parallel Alectryon documentation processing.
+
+## Overview
+
+The generator creates one dune rule per `.v` file in `theories/` and
+`contrib/`. Each rule:
+
+1. Runs `fcc` (Flèche Coq Compiler from coq-lsp) with the goaldump plugin to
+   extract proof goals
+2. Converts the goaldump JSON to Alectryon's JSON format using
+   `goaldump-to-alectryon.py` (in this directory)
+3. Runs Alectryon with the `coq.io.json` frontend to produce HTML
+
+## Why fcc instead of coq-lsp?
+
+Alectryon normally uses coq-lsp to extract proof states, but this is slow
+because coq-lsp is designed for interactive editing with incremental
+compilation. For batch documentation generation, `fcc` is much faster as it's
+optimized for single-pass compilation.
+
+alectryon will normally ask coq-lsp for each goal separately which takes way
+too long. By getting fcc (the Coq compiler based on internals of coq-lsp) to
+dump all the goals, we can process them as something alectryon can understand.
+
+## Generated Files
+
+For each `.v` file, the rule produces:
+- `<name>.html` - The Alectryon HTML documentation
+- `<name>.v.fcc.log` - Log output from fcc (useful for debugging)
+
+Files are output to `alectryon-html/` with flattened names (e.g.,
+`theories/WildCat/Core.v` becomes `theories.WildCat.Core.html`).
+
+## Usage
+
+```bash
+# Build all documentation
+dune build @alectryon
+
+# Build documentation for a single file
+dune build alectryon-html/theories.WildCat.Core.html
+```
+
+## Dependencies
+
+- `fcc` from coq-lsp with the goaldump plugin (`coq-lsp.plugin.goaldump`)
+- Python 3 with the Alectryon package (via `etc/alectryon/`)
+- `goaldump-to-alectryon.py` converter script (in this directory)
+
+## How It Works
+
+The rules are generated dynamically using dune's `dynamic_include` feature:
+
+1. `gen_alectryon_rules.exe` scans `theories/` and `contrib/` for `.v` files
+2. It outputs dune rules in S-expression format to `alectryon_rules.sexp`
+3. The main `dune` file includes these rules via `(dynamic_include
+   ../alectryon_rules.sexp)` in the `alectryon-html` subdirectory
+
+Each rule uses `(sandbox always)` to ensure parallel builds don't interfere
+with each other, since `fcc` writes intermediate files next to the source.
+
+## fcc Exit Codes
+
+Note: `fcc` may return exit code 1 even on successful compilation (due to "file
+not in workspace" warnings). The rules use `(with-accepted-exit-codes (or 0 1)
+...)` to handle this.

etc/gen-alectryon-rules/dune

@@ -0,0 +1,2 @@
+(executable
+ (name gen_alectryon_rules))

etc/gen-alectryon-rules/gen_alectryon_rules.ml

@@ -0,0 +1,63 @@
+(* Generate dune rules for parallel alectryon processing using fcc *)
+(* Rules are included from alectryon-html subdir, so paths use ../ prefix *)
+
+let find_v_files dirs =
+  let files = ref [] in
+  let rec walk dir =
+    let entries = Sys.readdir dir in
+    Array.iter (fun entry ->
+      let path = Filename.concat dir entry in
+      if Sys.is_directory path then
+        walk path
+      else if Filename.check_suffix entry ".v" then
+        files := path :: !files
+    ) entries
+  in
+  List.iter (fun dir -> if Sys.file_exists dir then walk dir) dirs;
+  List.sort String.compare !files
+
+let v_to_module path =
+  (* theories/Foo/Bar.v -> HoTT.Foo.Bar
+     contrib/Foo.v -> HoTT.Contrib.Foo *)
+  let base = Filename.chop_suffix path ".v" in
+  let parts = String.split_on_char '/' base in
+  match parts with
+  | "theories" :: rest -> "HoTT." ^ String.concat "." rest
+  | "contrib" :: rest -> "HoTT.Contrib." ^ String.concat "." rest
+  | _ -> String.concat "." parts
+
+let v_to_html path =
+  Printf.sprintf "%s.html" (v_to_module path)
+
+let print_rule vfile =
+  let html_target = v_to_html vfile in
+  let alectryon_json = vfile ^ ".alectryon.json" in
+  Printf.printf "\n(rule\n";
+  Printf.printf " (target %s)\n" html_target;
+  Printf.printf " (deps\n";
+  Printf.printf "  (sandbox always)\n";
+  Printf.printf "  ../%s\n" vfile;
+  Printf.printf "  ../_CoqProject\n";
+  Printf.printf "  (glob_files_rec ../theories/*.vo)\n";
+  Printf.printf "  (glob_files_rec ../contrib/*.vo)\n";
+  Printf.printf "  ../etc/gen-alectryon-rules/goaldump-to-alectryon.py\n";
+  Printf.printf "  (source_tree ../etc/alectryon))\n";
+  let log_target = v_to_module vfile ^ ".v.fcc.log" in
+  Printf.printf " (action\n";
+  Printf.printf "  (chdir ..\n";
+  Printf.printf "   (progn\n";
+  Printf.printf "    (with-outputs-to alectryon-html/%s (with-accepted-exit-codes (or 0 1) (run fcc --root=. --no_vo --plugin=coq-lsp.plugin.goaldump %s)))\n" log_target vfile;
+  Printf.printf "    (run python3 etc/gen-alectryon-rules/goaldump-to-alectryon.py %s -o %s)\n" vfile alectryon_json;
+  Printf.printf "    (run python3 etc/alectryon/alectryon.py --frontend coq.io.json %s --backend webpage -o alectryon-html/%s)))))\n" alectryon_json html_target
+
+let () =
+  let dirs = ["theories"; "contrib"] in
+  let files = find_v_files dirs in
+
+  (* Print individual rules *)
+  List.iter print_rule files;
+
+  (* Print umbrella alias *)
+  Printf.printf "\n(alias\n (name alectryon)\n (deps\n";
+  List.iter (fun vfile -> Printf.printf "  %s\n" (v_to_html vfile)) files;
+  Printf.printf "))\n"