generate alectryon rules for dune

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

.github/workflows/ci.yml

@@ -159,7 +159,7 @@ jobs:
 # - coqchk: Runs coqchk
 # - install: Tests install target
 
-  # alectryon doc job (using Nix for reproducible builds)
+  # alectryon doc job (using Nix + dune for reproducible builds)
   doc-alectryon:
     runs-on: ubuntu-latest
     steps:
@@ -171,14 +171,11 @@ jobs:
       with:
         primary-key: nix-${{ runner.os }}-${{ hashFiles('flake.lock') }}
         restore-prefixes-first-match: nix-${{ runner.os }}-
-    - name: add problem matchers
+    - name: Build alectryon docs with dune
       run: |
-        echo "::add-matcher::etc/coq-scripts/github/alectryon-error.json"
-    - name: Build and run alectryon
-      run: |
-        nix develop .#coq_9_0 -c make alectryon ALECTRYON_EXTRAFLAGS=--traceback
+        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:

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"