From 013b2293fdcda4a5090703f3678d8c94d49395e1 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 3 Feb 2026 11:50:31 +0100 Subject: [PATCH] proofnav: improve EasyCrypt error handling in Sphinx extension Make EasyCrypt failures non-fatal during documentation builds. Errors are now reported as Sphinx warnings instead of stopping the build, with the last EasyCrypt error message printed in the log. Additionally, all reported errors are properly located, either in the corresponding .rst source or in the referenced EasyCrypt file. --- doc/extensions/ecproofs/ecproofs.py | 133 +++++++++++++++++++++------- 1 file changed, 103 insertions(+), 30 deletions(-) diff --git a/doc/extensions/ecproofs/ecproofs.py b/doc/extensions/ecproofs/ecproofs.py index 6efe0f445..92a1571c3 100644 --- a/doc/extensions/ecproofs/ecproofs.py +++ b/doc/extensions/ecproofs/ecproofs.py @@ -1,5 +1,6 @@ # -------------------------------------------------------------- from __future__ import annotations +from typing import Any import docutils as du @@ -14,9 +15,13 @@ import subprocess as subp import tempfile + # ====================================================================== ROOT = os.path.dirname(__file__) +# ====================================================================== +logger = su.logging.getLogger(__name__) + # ====================================================================== class ProofnavNode(du.nodes.General, du.nodes.Element): @staticmethod @@ -37,58 +42,95 @@ def depart_proofnav_node_html(self, node: ProofnavNode): self.body.append(html) +# ====================================================================== +class EasyCryptError(se.SphinxError): + category = "easycrypt" + +# ====================================================================== +class EasyCrypt: + @staticmethod + def run(cmd, *, location: Any | None = None, warn_only: bool = True): + try: + proc = subp.run( + cmd, check = True, text = True, capture_output = True, + ) + logger.debug("Command stdout:\n%s", proc.stdout) + logger.debug("Command stderr:\n%s", proc.stderr) + + return True + + except subp.CalledProcessError as e: + msg = f"{cmd[0]} exited with code {e.returncode}" + + if e.stdout: + logger.debug("stdout:\n%s", e.stdout, location = location) + if e.stderr: + logger.debug("stderr:\n%s", e.stderr, location = location) + + logs = [x.split(maxsplit = 1) for x in e.stderr.splitlines()] + logs = [x[1] for x in logs if len(x) == 2 and x[0] == 'E'] + + for log in logs: + logger.error(log, location = location, type = EasyCryptError.category) + + logger.error(msg, location = location, type = EasyCryptError.category) + + raise EasyCryptError(msg) from e + # ====================================================================== class EasyCryptProofDirective(su.docutils.SphinxDirective): + TRAP_RE = r'\(\*\s*\$\s*\*\)\s*' + has_content = True option_spec = { 'title': su.docutils.directives.unchanged, } - def run(self): - env = self.state.document.settings.env + def find_trap(self, source: str): + location = (self.state.document.current_source, self.lineno) - rawcode = '\n'.join(self.content) + '\n' + if (trap := re.search(self.TRAP_RE, source, re.MULTILINE)) is None: + logger.error( + 'Cannot find the trap', + location = location, type = EasyCryptError.category) + raise EasyCryptError - # Find the trap - if (trap := re.search(r'\(\*\s*\$\s*\*\)\s*', rawcode, re.MULTILINE)) is None: - raise se.SphinxError('Cannot find the trap') - code = rawcode[:trap.start()] + rawcode[trap.end():] - - # Find the trap sentence number - sentences = [ - m.end() - 1 - for m in re.finditer(r'\.(\s+|\$)', code) - ] - sentence = bisect.bisect_left(sentences, trap.start()) + return trap + + def run_easycrypt(self, source: str): + location = (self.state.document.current_source, self.lineno) - # Run EasyCrypt and extract the proof trace with tempfile.TemporaryDirectory(delete = False) as tmpdir: ecfile = os.path.join(tmpdir, 'input.ec') ecofile = os.path.join(tmpdir, 'input.eco') + with open(ecfile, 'w') as ecstream: - ecstream.write(code) - subp.check_call( - ['easycrypt', 'compile', '-pragmas', 'Proofs:weak', '-trace', ecfile], - stdout = subp.DEVNULL, - stderr = subp.DEVNULL, + ecstream.write(source) + + EasyCrypt.run( + ['easycrypt', 'compile', '-script', '-pragmas', 'Proofs:weak', '-trace', ecfile], + location = location ) + with open(ecofile) as ecostream: - eco = json.load(ecostream) + return json.load(ecostream) - serial = env.new_serialno("proofnav") + def create_widget(self, code: str, sentence: int, eco: Any): + serial = self.state.document.settings.env.new_serialno("proofnav") uid = f"proofnav-{serial}" - # Create widget metadata - data = dict() - - data["source"] = code - data["sentenceEnds"] = [x["position"] for x in eco["trace"][1:]] - data["sentences"] = [ + sentences = [ dict(goals = x["goals"], message = x["messages"]) for x in eco["trace"][1:] ] - data["initialSentence"] = sentence - 1 + + data = dict( + source = code, + sentenceEnds = [x["position"] for x in eco["trace"][1:]], + sentences = sentences, + initialSentence = sentence - 1, + ) if 'title' in self.options: data['title'] = self.options['title'] @@ -97,8 +139,39 @@ def run(self): node["uid"] = uid node["json"] = json.dumps( data, ensure_ascii = False, separators = (",", ":"), indent = 2) + + return node - return [node] + def run(self): + try: + rawcode = '\n'.join(self.content) + '\n' + + # Find the trap and erase it + trap = self.find_trap(rawcode) + code = rawcode[:trap.start()] + rawcode[trap.end():] + + # Find the trap sentence number + sentences = [ + m.end() - 1 + for m in re.finditer(r'\.(\s+|\$)', code) + ] + sentence = bisect.bisect_left(sentences, trap.start()) + + # Run EasyCrypt and extract the proof trace + eco = self.run_easycrypt(code) + + # Create the widget + node = self.create_widget(code, sentence, eco) + return [node] + + except EasyCryptError: + self.state.document.settings.env.note_reread() + + fallback = du.nodes.literal_block( + "[easycrypt failed]", + "[easycrypt failed]", + ) + return [fallback] # ====================================================================== def on_builder_inited(app: sa.Sphinx):