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.

Author: strub

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