serapi: Add a "noexec" driver

Closes GH-52. Suggested-by: @gmalecha
cpitclaudel · Sep 3, 2021 · 6f4ae20 · 6f4ae20
1 parent f0ab88e
commit 6f4ae20
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/alectryon/core.py b/alectryon/core.py
@@ -342,6 +342,7 @@ def reset(self):
 DRIVERS_BY_LANGUAGE = {
     "coq": {
         "sertop": (".serapi", "SerAPI"),
+        "sertop_noexec": (".serapi", "SerAPI_noexec"),
         "coqc_time": (".coqc_time", "CoqcTime"),
     }
 }

diff --git a/alectryon/serapi.py b/alectryon/serapi.py
@@ -327,6 +327,19 @@ def annotate(self, chunks):
         with self as api:
             return [api.run(chunk) for chunk in chunks]
 
+class SerAPI_noexec(SerAPI):
+    """A variant of SerAPI that segments the code without executing it.
+
+    This runs faster, but the results don't include goals and messages."""
+
+    NAME = "Coq+SerAPI-noexec"
+    ID = "sertop_noexec"
+
+    def _exec(self, sid, chunk):
+        return []
+    def _goals(self, sid, chunk):
+        return []
+
 def annotate(chunks, sertop_args=(), fpath="-", binpath=None):
     r"""Annotate multiple `chunks` of Coq code.