You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Docs CI does not fail on broken ecproof examples #1111
The Build documentation workflow (.github/workflows/docs.yml) runs on every pull request, but a broken ecproof example does not fail it.
What happens
The ecproof directive (doc/extensions/ecproofs/ecproofs.py) requires a (*$*) trap marker in every example. When it is missing, the directive reports the problem through the Sphinx logger and emits an error node into the page. Sphinx counts logged errors as warnings, still writes the HTML, and exits 0. The workflow calls make -C doc sphinx-html with an empty SPHINXOPTS, so the job stays green.
doc/tactics/async-while.rst:44: ERROR: Cannot find the trap [easycrypt]
doc/tactics/hint-simplify.rst:148: ERROR: Cannot find the trap [easycrypt]
build succeeded, 3 warnings.
The hint-simplify.rst one has been fixed in PR #1110. The async-while.rst one is still on main, along with a docutils warning at doc/tactics/procstar.rst:2 (explicit markup ends without a blank line).
Proposed fix
Add the missing (*$*) trap to the async-while.rst example and fix the procstar.rst markup warning.
Pass SPHINXOPTS="-W --keep-going" to the Sphinx build in docs.yml, so any logged warning or error fails the job.
Step 1 must land first (or in the same PR), otherwise main goes red as soon as -W is enabled.
Activity