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.
Log of a green run (#33874648471, PR #1110):
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.
The
Build documentationworkflow (.github/workflows/docs.yml) runs on every pull request, but a brokenecproofexample does not fail it.What happens
The
ecproofdirective (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 callsmake -C doc sphinx-htmlwith an emptySPHINXOPTS, so the job stays green.Log of a green run (#33874648471, PR #1110):
The
hint-simplify.rstone has been fixed in PR #1110. Theasync-while.rstone is still onmain, along with a docutils warning atdoc/tactics/procstar.rst:2(explicit markup ends without a blank line).Proposed fix
(*$*)trap to theasync-while.rstexample and fix theprocstar.rstmarkup warning.SPHINXOPTS="-W --keep-going"to the Sphinx build indocs.yml, so any logged warning or error fails the job.Step 1 must land first (or in the same PR), otherwise
maingoes red as soon as-Wis enabled.