Merge pull request #1116 from LPCIC/refman

Add Sphinx reference manual

Author: gares

.github/workflows/doc.yml

@@ -34,22 +34,40 @@ jobs:
         opam repo add coq-dev https://coq.inria.fr/opam/core-dev
         opam repo add extra-dev https://coq.inria.fr/opam/extra-dev
         opam update
-        opam install rocq-core.9.0.0 vsrocq-language-server coq-core rocq-stdlib.9.0.0 coq-stdlib
+        opam install rocq-core.9.2.0 vsrocq-language-server coq-core rocq-stdlib.9.2.0 coq-stdlib
         opam install ./rocq-elpi.opam
         sudo apt-get update
         sudo apt-get install python3-pip -y
+        sudo pip3 install Sphinx sphinx-rtd-theme
 
-    - name: build doc
+    - name: build alectryon tutorials
       run: opam exec -- make doc
 
+    - name: build sphinx reference manual
+      run: opam exec -- make refman-build
+
+    # Combined GH Pages layout: the older Alectryon-rendered tutorials keep
+    # their existing root-level paths
+    # (https://lpcic.github.io/coq-elpi/tutorial_*.html -- already linked
+    # from both README.md and the new manual's own tutorial pages, via
+    # ".. seealso::" notes), and the new Sphinx reference manual (the one
+    # linked as "the reference manual" from README.md) is added alongside
+    # under refman/.
+    - name: combine docs for deployment
+      run: |
+        mkdir -p site
+        cp -r doc/. site/
+        mkdir -p site/refman
+        cp -r docs/build/. site/refman/
+
     - name: Save artifact
       uses: actions/upload-artifact@v4
       with:
-        path: doc
+        path: site
 
     - name: deploy
       uses: JamesIves/github-pages-deploy-action@4.1.4
       if: ${{ github.ref == 'refs/heads/master' }}
       with:
         branch: gh-pages
-        folder: doc
+        folder: site

.gitignore

@@ -32,6 +32,10 @@ src/rocq_elpi_vernacular_syntax.ml
 src/rocq_elpi_arg_syntax.ml
 src/rocq_elpi_builtins_HOAS.ml
 doc/
+docs/source/
+docs/build/
+docsenv/
+docs/base/__pycache__/
 
 Makefile.coq
 Makefile.coq.conf

.vscode/settings.json

@@ -33,4 +33,5 @@
     "ocaml.server.args": [
         "--fallback-read-dot-merlin"
     ],
+    "vscode-as-git-mergetool.settingsAssistantOnStartup": false,
 }

Makefile

@@ -88,6 +88,25 @@ doc:
 			$(tut) &&) true
 	@cp etc/tracer.png doc/
 
+# Sphinx-based reference manual (docs/base -> docs/source -> docs/build).
+# `.. rocqtop::` blocks in docs/base/**/*.rst run through a real `rocq top`
+# with rocq-elpi loaded, so rocq-elpi must be installed into the opam switch
+# `rocq top` resolves against (not just dune-built-in-place), and
+# builtin-doc/*.elpi must exist on disk (read by docs/base/_roles_elpi.py).
+refman-build:
+	$(call dune,build) -p rocq-elpi @install
+	$(call dune,build) builtin-doc
+	$(call dune,install) rocq-elpi
+	rm -rf docs/source docs/build
+	cp -r docs/base docs/source
+	sed -i "s/@@VERSION@@/$$(git describe --always)/" docs/source/conf.py
+	sphinx-build -q -W -b html docs/source docs/build
+.PHONY: refman-build
+
+refman-serve: refman-build
+	cd docs/build && python3 -m http.server 8000
+.PHONY: refman-serve
+
 clean:
 	$(call dune,clean)
 .PHONY: clean

README.md

@@ -242,7 +242,7 @@ X s>= Y :- ge_ X Y.
 
 %  -- Standard data types (supported in the FFI) --
 
-kind list type -> type.
+data list A.
 
 builtin symb (::) : X -> list X -> list X = "core".
 
@@ -266,8 +266,8 @@ func snd  pair A B -> B.
 snd (pr _ B) B.
 
 
-kind triple type -> type -> type -> type.
-type triple A -> B -> C -> triple A B C.
+data triple A B C.
+symb triple A -> B -> C -> triple A B C.
 
 func triple_1 triple A B C -> A.
 triple_1 (triple A _ _) A.
@@ -1077,8 +1077,8 @@ builtin func std.loc.set.partition std.loc.set,
                                   (func loc) -> std.loc.set, std.loc.set.
 
 #line 1 "builtin_map.elpi"
-kind std.map type -> type -> type.
-type std.map std.map.private.map K V -> (func K, K -> cmp) -> std.map K V.
+data std.map K V.
+symb std.map std.map.private.map K V -> (func K, K -> cmp) -> std.map K V.
 
 namespace std.map {
 
@@ -1105,9 +1105,9 @@ bindings (std.map M _) L :- private.bindings M [] L.
 namespace private {
 
 % Taken from OCaml's map.ml
-kind map type -> type -> type.
-type empty map K V.
-type node map K V -> K -> V -> map K V -> int -> map K V.
+data map K V.
+symb empty map K V.
+symb node map K V -> K -> V -> map K V -> int -> map K V.
 
 func height map K V -> int.
 height empty 0.
@@ -1193,8 +1193,8 @@ bindings (node L V D R _) X X1 :-
 
 % Fast maps only work ground terms but do not perform occur check
 
-kind std.fmap type -> type -> type.
-type std.fmap std.fmap.private.map K V -> (func K, K -> cmp) -> std.fmap K V.
+data std.fmap K V.
+symb std.fmap std.fmap.private.map K V -> (func K, K -> cmp) -> std.fmap K V.
 
 namespace std.fmap {
 
@@ -1233,9 +1233,9 @@ func assert-ground A.
 assert-ground A :- std.assert! (ground_term A) "std.fmap: not ground".
 
 % Taken from OCaml's map.ml
-kind map type -> type -> type.
-type empty map K V.
-type node map K V -> K -> V -> map K V -> int -> map K V.
+data map K V.
+symb empty map K V.
+symb node map K V -> K -> V -> map K V -> int -> map K V.
 
 func height map K V -> int.
 height empty 0.
@@ -1321,8 +1321,8 @@ bindings (node L V D R _) X X1 :-
 
 
 #line 1 "builtin_set.elpi"
-kind std.set type -> type.
-type std.set std.set.private.set E -> (func E, E -> cmp) -> std.set E.
+data std.set E.
+symb std.set std.set.private.set E -> (func E, E -> cmp) -> std.set E.
 
 namespace std.set {
 
@@ -1352,9 +1352,9 @@ elements (std.set M _) L :- private.elements M [] L.
 namespace private {
 
 % Taken from OCaml's set.ml
-kind set type -> type.
-type empty set E.
-type node set E -> E -> set E -> int -> set E.
+data set E.
+symb empty set E.
+symb node set E -> E -> set E -> int -> set E.
 
 func height set E -> int.
 height empty 0.
@@ -1443,8 +1443,8 @@ elements (node L E R _) Acc X :-
 
 % Fast sets only work ground terms but do not perform occur check
 
-kind std.fset type -> type.
-type std.fset std.fset.private.set E -> (func E, E -> cmp) -> std.fset E.
+data std.fset E.
+symb std.fset std.fset.private.set E -> (func E, E -> cmp) -> std.fset E.
 
 namespace std.fset {
 
@@ -1483,9 +1483,9 @@ func assert-ground A.
 assert-ground A :- std.assert! (ground_term A) "std.fset: not ground".
 
 % Taken from OCaml's set.ml
-kind set type -> type.
-type empty set E.
-type node set E -> E -> set E -> int -> set E.
+data set E.
+symb empty set E.
+symb node set E -> E -> set E -> int -> set E.
 
 func height set E -> int.
 height empty 0.

builtin-doc/elpi-builtin.elpi

@@ -0,0 +1,89 @@
+# Rocq-Elpi reference manual
+
+This directory holds the Sphinx-based reference manual published at
+<https://lpcic.github.io/coq-elpi/refman/>.
+
+## Source layout
+
+Only `docs/base/` is tracked by git; everything else under `docs/` is
+generated and gitignored.
+
+- `docs/base/conf.py` — Sphinx configuration: registers the custom
+  lexers/roles/directive below, sets the theme (`sphinx_rtd_theme`), etc.
+- `docs/base/_pygments_elpi.py` — a Pygments lexer for Elpi, and for Rocq
+  with embedded `lp:{{ ... }}` Elpi quotations, used both for
+  `.. code-block::`/`:e:`-style highlighting and by `_rocqtop_elpi.py` below.
+- `docs/base/_roles_elpi.py` — custom roles (`:builtin:`, `:stdlib:`,
+  `:type:`, `:lib:`, ...) that link a predicate/type/macro name to its
+  declaration in `builtin-doc/*.elpi` or `elpi/*.elpi`, resolved locally via
+  `git log` (no network access at build time).
+- `docs/base/_rocqtop_elpi.py` — the `.. rocqtop::` directive: spawns a real
+  `rocq top` process and feeds it the block's Rocq/Elpi sentences one at a
+  time, rendering the sentence together with its *actually captured* output.
+  This is what every tutorial/example page uses for its code samples instead
+  of static transcripts, so a sample that no longer compiles breaks the
+  build rather than silently going stale.
+- `docs/base/index.rst`, `getting-started.rst`, `apps.rst`,
+  `tutorials/`, `reference/`, `examples/` — the manual's actual content.
+- `docs/base/_static/custom.css` — small CSS additions on top of the theme
+  (ANSI colors for `.. rocqtop::` output, Elpi-specific token colors, ...).
+
+## Building
+
+```
+make refman-build
+```
+
+(from the repository root) does, in order:
+
+1. `dune build -p rocq-elpi @install` — builds the `.install` files
+   `dune install` (next step) needs; without it, `dune install` fails with
+   `<package>.install are missing` unless some earlier, unrelated full
+   `dune build` happened to already produce them.
+2. `dune build builtin-doc` — `_roles_elpi.py` reads `builtin-doc/*.elpi`
+   straight off disk, so it must exist and be up to date.
+3. `dune install rocq-elpi` — installs Rocq-Elpi into the current opam
+   switch. This is required (not just building it in place) because
+   `.. rocqtop::` spawns a real `rocq top` that loads `From elpi Require
+   Import elpi.` the same way an end user's opam switch would.
+4. Copies `docs/base/` to `docs/source/` (gitignored), substituting
+   `@@VERSION@@` in `conf.py` with `git describe --always`.
+5. Runs `sphinx-build -q -W -b html docs/source docs/build`. `-W` turns
+   every warning into a hard build failure — a broken `:builtin:`/`:doc:`
+   reference, a `.. rocqtop::` sentence that errors out, or a dangling
+   toctree entry all fail the build rather than degrading quietly.
+
+`docs/source/` and `docs/build/` are both deleted and recreated on every
+run; never edit files there by hand.
+
+Requirements beyond the repository's usual opam/dune setup: `Sphinx` and
+`sphinx-rtd-theme` (`pip install Sphinx sphinx-rtd-theme`), installed into
+whichever Python `sphinx-build` resolves to on `$PATH`.
+
+To build and preview locally:
+
+```
+make refman-serve   # builds, then serves docs/build/ on http://localhost:8000
+```
+
+## Deployment
+
+`.github/workflows/doc.yml` runs on every push/PR to `master`. On `master`
+it builds **two** things and deploys them together to the `gh-pages` branch
+(published at <https://lpcic.github.io/coq-elpi/>):
+
+- `make doc` — the older per-tutorial pages rendered with
+  [Alectryon](https://github.com/cpitclaudel/alectryon) from
+  `examples/tutorial_*.v`, output to `doc/`. These keep their original,
+  already-linked-elsewhere paths, e.g.
+  `https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html` — every new
+  manual tutorial page links back to its Alectryon-rendered original via a
+  `.. seealso::` note, so these paths must not move.
+- `make refman-build` — this Sphinx manual, output to `docs/build/`, copied
+  into the deployed site under `refman/`, i.e.
+  `https://lpcic.github.io/coq-elpi/refman/`.
+
+The workflow's `combine docs for deployment` step lays both out under one
+`site/` directory (`doc/*` at the root, `docs/build/*` under `site/refman/`)
+before handing it to `JamesIves/github-pages-deploy-action`, which force-pushes
+`site/` as the full contents of the `gh-pages` branch.