Refman skeleton.

.github/workflows/docs.yml

@@ -0,0 +1,104 @@
+name: Build documentation
+
+on:
+  push:
+    branches:
+      - "main"
+  pull_request:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Set up Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: "20"
+
+      - name: Install npm dependencies
+        run: |
+          make -C doc ecproof-deps
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.13"
+
+      - name: Install Python dependencies
+        run: |
+          make -C doc sphinx-deps
+
+      - name: Set-up OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 5.4
+          opam-disable-sandboxing: true
+          dune-cache: true
+
+      - name: Install EasyCrypt dependencies
+        run: |
+          opam pin add -n easycrypt .
+          opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
+          opam install --deps-only easycrypt
+
+      - name: Compile & Install EasyCrypt
+        run: |
+          opam exec -- make PROFILE=release install
+
+      - name: Build Sphinx HTML
+        run: |
+          opam exec -- make -C doc ecproof-bundle sphinx-html
+
+      - name: Upload Pages artifact
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: doc/_build/html
+
+  deploy:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+
+    steps:
+    - name: Deploy documentation
+      env:
+        PAGES_TOKEN: ${{ secrets.PAGES_REPO_TOKEN }}
+        PAGES_REPO: EasyCrypt/refman
+        TARGET_DIR: refman
+        BUILD_DIR: doc/_build/html
+
+      run: |
+        set -euo pipefail
+
+        git config --global user.name  "github-actions[bot]"
+        git config --global user.email "github-actions[bot]@users.noreply.github.com"
+
+        git clone --depth 1 https://x-access-token:${PAGES_TOKEN}@github.com/${PAGES_REPO}.git pages-repo
+
+        rm -rf "pages-repo/${TARGET_DIR}"
+        mkdir -p "pages-repo/${TARGET_DIR}"
+        touch "pages-repo/${TARGET_DIR}"/.keep
+
+        cp -a "${BUILD_DIR}/." "pages-repo/${TARGET_DIR}/"
+
+        git -C pages-repo add -A
+
+        if git -C pages-repo diff --cached --quiet; then
+          echo "No changes to deploy."
+          exit 0
+        fi
+
+        git -C pages-repo commit -m "Update docs: ${GITHUB_REPOSITORY}@${GITHUB_SHA}"
+        git -C pages-repo push origin main

doc/.gitignore

@@ -0,0 +1,2 @@
+__pycache__/
+_build/

doc/Makefile

@@ -0,0 +1,45 @@
+# -*- Makefile -*-
+
+# ------------------------------------------------------------------------
+SPHINXBUILD ?= sphinx-build
+SPHINXOPTS  ?=
+SOURCEDIR    = .
+BUILDDIR     = _build
+NPM         ?= npm
+
+# ------------------------------------------------------------------------
+.PHONY:
+
+default:
+	@echo "make [ecproof-deps | ecproof-bundle| sphinx-html]" >&2
+
+# ------------------------------------------------------------------------
+.PHONY: sphinx-help sphinx-deps __force__
+
+sphinx-help:
+	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS)
+
+sphinx-deps:
+	pip install -r requirements.txt
+
+sphinx-%: __force__
+	@$(SPHINXBUILD) -M $* "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS)
+
+# ------------------------------------------------------------------------
+.PHONY: ecproof-deps ecproof-bundle
+
+ECPROOFDIR = extensions/ecproofs/proofnav
+
+ecproof-deps:
+	$(NPM) --prefix="$(ECPROOFDIR)" install
+
+ecproof-bundle:
+	$(NPM) --prefix="$(ECPROOFDIR)" run build
+
+# ------------------------------------------------------------------------
+clean:
+	rm -rf _build
+	rm -rf "$(ECPROOFDIR)"/dist
+
+mrproper: clean
+	rm -rf "$(ECPROOFDIR)"/node_modules

doc/conf.py

@@ -0,0 +1,38 @@
+# Configuration file for the Sphinx documentation builder.
+#
+# For the full list of built-in configuration values, see the documentation:
+# https://www.sphinx-doc.org/en/master/usage/configuration.html
+
+import pathlib
+import sys
+
+# -- Project information -----------------------------------------------------
+# https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
+
+project = 'EasyCrypt refman'
+copyright = '2026, EasyCrypt development team'
+author = 'EasyCrypt development team'
+
+# -- General configuration ---------------------------------------------------
+# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration
+
+EXTENSIONS = pathlib.Path('extensions').resolve()
+for x in ['ecpygment', 'ecproofs']:
+    sys.path.append(str(EXTENSIONS / x))
+
+extensions = [
+    'sphinx_rtd_theme',
+    'sphinx_design',
+    'ecpygment',
+    'ecproofs',
+]
+
+templates_path = ['_templates']
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+
+# -- Options for HTML output -------------------------------------------------
+# https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output
+
+html_theme = 'sphinx_rtd_theme'
+html_static_path = ['_static']
+highlight_language = 'easycrypt'

doc/extensions/ecproofs/ecproofs.py

@@ -0,0 +1,141 @@
+# --------------------------------------------------------------
+from __future__ import annotations
+
+import docutils as du
+
+import sphinx.application as sa
+import sphinx.errors      as se
+import sphinx.util        as su
+
+import bisect
+import json
+import os
+import re
+import subprocess as subp
+import tempfile
+
+# ======================================================================
+ROOT = os.path.dirname(__file__)
+
+# ======================================================================
+class ProofnavNode(du.nodes.General, du.nodes.Element):
+  @staticmethod
+  def visit_proofnav_node_html(self, node: ProofnavNode):
+    pass
+
+  @staticmethod
+  def depart_proofnav_node_html(self, node: ProofnavNode):
+    uid  = node["uid"]
+    json = node["json"]
+
+    html = f"""
+<div class="proofnav-sphinx">
+  <div id="{uid}" class="proofnav-mount"></div>
+  <script type="application/json" id="{uid}-data">{json}</script>
+</div>
+"""
+
+    self.body.append(html)
+
+# ======================================================================
+class EasyCryptProofDirective(su.docutils.SphinxDirective):
+  has_content = True
+
+  option_spec = {
+    'title': su.docutils.directives.unchanged,
+  }
+
+  def run(self):
+    env = self.state.document.settings.env
+
+    rawcode = '\n'.join(self.content) + '\n'
+
+    # Find the trap
+    if (trap := re.search(r'\(\*\s*\$\s*\*\)\s*', rawcode, re.MULTILINE)) is None:
+      raise se.SphinxError('Cannot find the trap')
+    code = rawcode[:trap.start()] + rawcode[trap.end():]
+
+    # Find the trap sentence number
+    sentences = [
+      m.end() - 1
+      for m in re.finditer(r'\.(\s+|\$)', code)
+    ]
+    sentence = bisect.bisect_left(sentences, trap.start())
+
+    # Run EasyCrypt and extract the proof trace
+    with tempfile.TemporaryDirectory(delete = False) as tmpdir:
+      ecfile  = os.path.join(tmpdir, 'input.ec')
+      ecofile = os.path.join(tmpdir, 'input.eco')
+      with open(ecfile, 'w') as ecstream:
+        ecstream.write(code)
+      subp.check_call(
+        ['easycrypt', 'compile', '-pragmas', 'Proofs:weak', '-trace', ecfile],
+        stdout = subp.DEVNULL,
+        stderr = subp.DEVNULL,
+      )
+      with open(ecofile) as ecostream:
+        eco = json.load(ecostream)
+
+    serial = env.new_serialno("proofnav")
+    uid = f"proofnav-{serial}"
+
+    # Create widget metadata
+    data = dict()
+
+    data["source"] = code
+    data["sentenceEnds"] = [x["position"] for x in eco["trace"][1:]]
+    data["sentences"] = [
+      dict(goals = x["goals"], message = x["messages"])
+      for x in eco["trace"][1:]
+    ]
+    data["initialSentence"] = sentence - 1
+
+    if 'title' in self.options:
+      data['title'] = self.options['title']      
+
+    node = ProofnavNode()
+    node["uid"] = uid
+    node["json"] = json.dumps(data, ensure_ascii = False, separators = (",", ":"))
+
+    return [node]
+
+# ======================================================================
+def on_builder_inited(app: sa.Sphinx):
+  out_dir = os.path.join(app.outdir, "_static", "proofnav")
+  os.makedirs(out_dir, exist_ok = True)
+
+  js  = os.path.join(ROOT, "proofnav", "dist", "proofnav.bundle.js")
+  css = os.path.join(ROOT, "proofnav", "proofnav.css")
+
+  if not os.path.exists(js):
+    raise se.SphinxError(
+      "proofnav: bundle not found. Run the frontend build to generate "
+      f"{js}"
+    )
+
+  su.fileutil.copy_asset(js, out_dir)
+  su.fileutil.copy_asset(js + ".map", out_dir)
+  su.fileutil.copy_asset(css, out_dir)
+
+# ======================================================================
+def setup(app: sa.Sphinx) -> su.typing.ExtensionMetadata:
+  app.add_node(
+    ProofnavNode,
+    html = (
+      ProofnavNode.visit_proofnav_node_html,
+      ProofnavNode.depart_proofnav_node_html,
+    )
+  )
+
+  app.add_js_file("proofnav/proofnav.bundle.js", defer = "defer")
+  app.add_css_file("proofnav/proofnav.css")
+
+  app.connect("builder-inited", on_builder_inited)
+
+  app.add_directive('ecproof', EasyCryptProofDirective)
+
+  return {
+    'version': '0.1',
+    'parallel_read_safe': True,
+    'parallel_write_safe': True,
+  }

doc/extensions/ecproofs/proofnav/.gitignore

@@ -0,0 +1,2 @@
+/dist/
+/node_modules/