Skip to content

Commit a13288a

Browse files
strubstrub
committed
start playing with Sphinx + EC
1 parent 83952e3 commit a13288a

20 files changed

Lines changed: 2004 additions & 0 deletions

File tree

‎.github/workflows/docs.yml‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
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+
50+
- name: Install EasyCrypt dependencies
51+
run: |
52+
opam pin add -n easycrypt .
53+
opam install --deps-only --depext-only --confirm-level=unsafe-yes easycrypt
54+
opam install --deps-only easycrypt
55+
56+
- name: Compile & Install EasyCrypt
57+
run: |
58+
opam exec -- make PROFILE=release install
59+
60+
- name: Build Sphinx HTML
61+
run: |
62+
opam exec -- make -C doc ecproof-bundle sphinx-html
63+
64+
- name: Upload Pages artifact
65+
uses: actions/upload-pages-artifact@v3
66+
with:
67+
path: doc/_build/html

‎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/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: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
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(['easycrypt', 'compile', '-trace', ecfile])
72+
with open(ecofile) as ecostream:
73+
eco = json.load(ecostream)
74+
75+
serial = env.new_serialno("proofnav")
76+
uid = f"proofnav-{serial}"
77+
78+
# Create widget metadata
79+
data = dict()
80+
81+
data["source"] = code
82+
data["sentenceEnds"] = [x["position"] for x in eco["trace"][1:]]
83+
data["sentences"] = [
84+
dict(goals = x["goals"], message = x["messages"])
85+
for x in eco["trace"][1:]
86+
]
87+
data["initialSentence"] = sentence - 1
88+
89+
if 'title' in self.options:
90+
data['title'] = self.options['title']
91+
92+
node = ProofnavNode()
93+
node["uid"] = uid
94+
node["json"] = json.dumps(data, ensure_ascii = False, separators = (",", ":"))
95+
96+
return [node]
97+
98+
# ======================================================================
99+
def on_builder_inited(app: sa.Sphinx):
100+
out_dir = os.path.join(app.outdir, "_static", "proofnav")
101+
os.makedirs(out_dir, exist_ok = True)
102+
103+
js = os.path.join(ROOT, "proofnav", "dist", "proofnav.bundle.js")
104+
css = os.path.join(ROOT, "proofnav", "proofnav.css")
105+
106+
if not os.path.exists(js):
107+
raise se.SphinxError(
108+
"proofnav: bundle not found. Run the frontend build to generate "
109+
f"{js}"
110+
)
111+
112+
su.fileutil.copy_asset(js, out_dir)
113+
su.fileutil.copy_asset(js + ".map", out_dir)
114+
su.fileutil.copy_asset(css, out_dir)
115+
116+
# ======================================================================
117+
def setup(app: sa.Sphinx) -> su.typing.ExtensionMetadata:
118+
app.add_node(
119+
ProofnavNode,
120+
html = (
121+
ProofnavNode.visit_proofnav_node_html,
122+
ProofnavNode.depart_proofnav_node_html,
123+
)
124+
)
125+
126+
app.add_js_file("proofnav/proofnav.bundle.js", defer = "defer")
127+
app.add_css_file("proofnav/proofnav.css")
128+
129+
app.connect("builder-inited", on_builder_inited)
130+
131+
app.add_directive('ecproof', EasyCryptProofDirective)
132+
133+
return {
134+
'version': '0.1',
135+
'parallel_read_safe': True,
136+
'parallel_write_safe': True,
137+
}

‎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)