Skip to content

Docs CI does not fail on broken ecproof examples #1111

Description

@strub

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

  1. Add the missing (*$*) trap to the async-while.rst example and fix the procstar.rst markup warning.
  2. 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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions