Skip to content

Commit 1bc6167

Browse files
strubstrub
committed
Refman skeleton.
Uses Sphinx + an extension that generates proofs viewable and navigable directly in the browser.
1 parent 2aa7329 commit 1bc6167

File tree

21 files changed

+2045
-0
lines changed

21 files changed

+2045
-0
lines changed

‎.github/workflows/docs.yml‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
name: Build documentation
2+
3+
on:
4+
push:
5+
branches:
6+
- "main"
7+
pull_request:
8+
9+
permissions:
10+
contents: read
11+
pages: write
12+
id-token: write
13+
14+
concurrency:
15+
group: "pages"
16+
cancel-in-progress: true
17+
18+
jobs:
19+
build:
20+
runs-on: ubuntu-latest
21+
22+
steps:
23+
- name: Checkout
24+
uses: actions/checkout@v4
25+
26+
- name: Set up Node.js
27+
uses: actions/setup-node@v4
28+
with:
29+
node-version: "20"
30+
31+
- name: Install npm dependencies
32+
run: |
33+
make -C doc ecproof-deps
34+
35+
- name: Set up Python
36+
uses: actions/setup-python@v5
37+
with:
38+
python-version: "3.13"
39+
40+
- name: Install Python dependencies
41+
run: |
42+
make -C doc sphinx-deps
43+
44+
- name: Set-up OCaml
45+
uses: ocaml/setup-ocaml@v3
46+
with:
47+
ocaml-compiler: 5.4
48+
opam-disable-sandboxing: true
49+
dune-cache: true
50+
51+
- name: Install EasyCrypt dependencies
52+
run: |
53+
opam pin add -n easycrypt .
54+
opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
55+
opam install --deps-only easycrypt
56+
57+
- name: Compile & Install EasyCrypt
58+
run: |
59+
opam exec -- make PROFILE=release install
60+
61+
- name: Build Sphinx HTML
62+
run: |
63+
opam exec -- make -C doc ecproof-bundle sphinx-html
64+
65+
- name: Upload Pages artifact
66+
uses: actions/upload-pages-artifact@v3
67+
with:
68+
path: doc/_build/html
69+
70+
deploy:
71+
runs-on: ubuntu-latest
72+
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
73+
74+
steps:
75+
- name: Deploy documentation
76+
env:
77+
PAGES_TOKEN: ${{ secrets.PAGES_REPO_TOKEN }}
78+
PAGES_REPO: EasyCrypt/refman
79+
TARGET_DIR: refman
80+
BUILD_DIR: doc/_build/html
81+
82+
run: |
83+
set -euo pipefail
84+
85+
git config --global user.name "github-actions[bot]"
86+
git config --global user.email "github-actions[bot]@users.noreply.github.com"
87+
88+
git clone --depth 1 https://x-access-token:${PAGES_TOKEN}@github.com/${PAGES_REPO}.git pages-repo
89+
90+
rm -rf "pages-repo/${TARGET_DIR}"
91+
mkdir -p "pages-repo/${TARGET_DIR}"
92+
touch "pages-repo/${TARGET_DIR}"/.keep
93+
94+
cp -a "${BUILD_DIR}/." "pages-repo/${TARGET_DIR}/"
95+
96+
git -C pages-repo add -A
97+
98+
if git -C pages-repo diff --cached --quiet; then
99+
echo "No changes to deploy."
100+
exit 0
101+
fi
102+
103+
git -C pages-repo commit -m "Update docs: ${GITHUB_REPOSITORY}@${GITHUB_SHA}"
104+
git -C pages-repo push origin main

‎doc/.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
__pycache__/
2+
_build/

‎doc/Makefile‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
# -*- Makefile -*-
2+
3+
# ------------------------------------------------------------------------
4+
SPHINXBUILD ?= sphinx-build
5+
SPHINXOPTS ?=
6+
SOURCEDIR = .
7+
BUILDDIR = _build
8+
NPM ?= npm
9+
10+
# ------------------------------------------------------------------------
11+
.PHONY:
12+
13+
default:
14+
@echo "make [ecproof-deps | ecproof-bundle| sphinx-html]" >&2
15+
16+
# ------------------------------------------------------------------------
17+
.PHONY: sphinx-help sphinx-deps __force__
18+
19+
sphinx-help:
20+
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS)
21+
22+
sphinx-deps:
23+
pip install -r requirements.txt
24+
25+
sphinx-%: __force__
26+
@$(SPHINXBUILD) -M $* "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(SPHINXOPTS)
27+
28+
# ------------------------------------------------------------------------
29+
.PHONY: ecproof-deps ecproof-bundle
30+
31+
ECPROOFDIR = extensions/ecproofs/proofnav
32+
33+
ecproof-deps:
34+
$(NPM) --prefix="$(ECPROOFDIR)" install
35+
36+
ecproof-bundle:
37+
$(NPM) --prefix="$(ECPROOFDIR)" run build
38+
39+
# ------------------------------------------------------------------------
40+
clean:
41+
rm -rf _build
42+
rm -rf "$(ECPROOFDIR)"/dist
43+
44+
mrproper: clean
45+
rm -rf "$(ECPROOFDIR)"/node_modules

‎doc/_static/.keep‎

Whitespace-only changes.

‎doc/conf.py‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
# Configuration file for the Sphinx documentation builder.
2+
#
3+
# For the full list of built-in configuration values, see the documentation:
4+
# https://www.sphinx-doc.org/en/master/usage/configuration.html
5+
6+
import pathlib
7+
import sys
8+
9+
# -- Project information -----------------------------------------------------
10+
# https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
11+
12+
project = 'EasyCrypt refman'
13+
copyright = '2026, EasyCrypt development team'
14+
author = 'EasyCrypt development team'
15+
16+
# -- General configuration ---------------------------------------------------
17+
# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration
18+
19+
EXTENSIONS = pathlib.Path('extensions').resolve()
20+
for x in ['ecpygment', 'ecproofs']:
21+
sys.path.append(str(EXTENSIONS / x))
22+
23+
extensions = [
24+
'sphinx_rtd_theme',
25+
'sphinx_design',
26+
'ecpygment',
27+
'ecproofs',
28+
]
29+
30+
templates_path = ['_templates']
31+
exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
32+
33+
# -- Options for HTML output -------------------------------------------------
34+
# https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output
35+
36+
html_theme = 'sphinx_rtd_theme'
37+
html_static_path = ['_static']
38+
highlight_language = 'easycrypt'

‎doc/extensions/ecproofs/ecproofs.py‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
# --------------------------------------------------------------
2+
from __future__ import annotations
3+
4+
import docutils as du
5+
6+
import sphinx.application as sa
7+
import sphinx.errors as se
8+
import sphinx.util as su
9+
10+
import bisect
11+
import json
12+
import os
13+
import re
14+
import subprocess as subp
15+
import tempfile
16+
17+
# ======================================================================
18+
ROOT = os.path.dirname(__file__)
19+
20+
# ======================================================================
21+
class ProofnavNode(du.nodes.General, du.nodes.Element):
22+
@staticmethod
23+
def visit_proofnav_node_html(self, node: ProofnavNode):
24+
pass
25+
26+
@staticmethod
27+
def depart_proofnav_node_html(self, node: ProofnavNode):
28+
uid = node["uid"]
29+
json = node["json"]
30+
31+
html = f"""
32+
<div class="proofnav-sphinx">
33+
<div id="{uid}" class="proofnav-mount"></div>
34+
<script type="application/json" id="{uid}-data">{json}</script>
35+
</div>
36+
"""
37+
38+
self.body.append(html)
39+
40+
# ======================================================================
41+
class EasyCryptProofDirective(su.docutils.SphinxDirective):
42+
has_content = True
43+
44+
option_spec = {
45+
'title': su.docutils.directives.unchanged,
46+
}
47+
48+
def run(self):
49+
env = self.state.document.settings.env
50+
51+
rawcode = '\n'.join(self.content) + '\n'
52+
53+
# Find the trap
54+
if (trap := re.search(r'\(\*\s*\$\s*\*\)\s*', rawcode, re.MULTILINE)) is None:
55+
raise se.SphinxError('Cannot find the trap')
56+
code = rawcode[:trap.start()] + rawcode[trap.end():]
57+
58+
# Find the trap sentence number
59+
sentences = [
60+
m.end() - 1
61+
for m in re.finditer(r'\.(\s+|\$)', code)
62+
]
63+
sentence = bisect.bisect_left(sentences, trap.start())
64+
65+
# Run EasyCrypt and extract the proof trace
66+
with tempfile.TemporaryDirectory(delete = False) as tmpdir:
67+
ecfile = os.path.join(tmpdir, 'input.ec')
68+
ecofile = os.path.join(tmpdir, 'input.eco')
69+
with open(ecfile, 'w') as ecstream:
70+
ecstream.write(code)
71+
subp.check_call(
72+
['easycrypt', 'compile', '-pragmas', 'Proofs:weak', '-trace', ecfile],
73+
stdout = subp.DEVNULL,
74+
stderr = subp.DEVNULL,
75+
)
76+
with open(ecofile) as ecostream:
77+
eco = json.load(ecostream)
78+
79+
serial = env.new_serialno("proofnav")
80+
uid = f"proofnav-{serial}"
81+
82+
# Create widget metadata
83+
data = dict()
84+
85+
data["source"] = code
86+
data["sentenceEnds"] = [x["position"] for x in eco["trace"][1:]]
87+
data["sentences"] = [
88+
dict(goals = x["goals"], message = x["messages"])
89+
for x in eco["trace"][1:]
90+
]
91+
data["initialSentence"] = sentence - 1
92+
93+
if 'title' in self.options:
94+
data['title'] = self.options['title']
95+
96+
node = ProofnavNode()
97+
node["uid"] = uid
98+
node["json"] = json.dumps(data, ensure_ascii = False, separators = (",", ":"))
99+
100+
return [node]
101+
102+
# ======================================================================
103+
def on_builder_inited(app: sa.Sphinx):
104+
out_dir = os.path.join(app.outdir, "_static", "proofnav")
105+
os.makedirs(out_dir, exist_ok = True)
106+
107+
js = os.path.join(ROOT, "proofnav", "dist", "proofnav.bundle.js")
108+
css = os.path.join(ROOT, "proofnav", "proofnav.css")
109+
110+
if not os.path.exists(js):
111+
raise se.SphinxError(
112+
"proofnav: bundle not found. Run the frontend build to generate "
113+
f"{js}"
114+
)
115+
116+
su.fileutil.copy_asset(js, out_dir)
117+
su.fileutil.copy_asset(js + ".map", out_dir)
118+
su.fileutil.copy_asset(css, out_dir)
119+
120+
# ======================================================================
121+
def setup(app: sa.Sphinx) -> su.typing.ExtensionMetadata:
122+
app.add_node(
123+
ProofnavNode,
124+
html = (
125+
ProofnavNode.visit_proofnav_node_html,
126+
ProofnavNode.depart_proofnav_node_html,
127+
)
128+
)
129+
130+
app.add_js_file("proofnav/proofnav.bundle.js", defer = "defer")
131+
app.add_css_file("proofnav/proofnav.css")
132+
133+
app.connect("builder-inited", on_builder_inited)
134+
135+
app.add_directive('ecproof', EasyCryptProofDirective)
136+
137+
return {
138+
'version': '0.1',
139+
'parallel_read_safe': True,
140+
'parallel_write_safe': True,
141+
}

‎doc/extensions/ecproofs/proofnav/.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
/dist/
2+
/node_modules/

0 commit comments

Comments
 (0)