cli, docutils: Allow users to run Coq code using coqc -time

README.rst

@@ -497,12 +497,12 @@ When compiling reStructuredText documents, you can add custom SerAPI arguments i
 
    :alectryon/serapi/args: -R . Lib -I mldir
 
-To set SerAPI's arguments for all input files, modify ``AlectryonTransform.SERTOP_ARGS`` in ``alectryon.docutils``.  Here's an example that you could use in a Sphinx config file::
+To set SerAPI's arguments for all input files, modify ``AlectryonTransform.DRIVER_ARGS["sertop"]`` in ``alectryon.docutils``.  Here's an example that you could use in a Sphinx config file::
 
    from alectryon.docutils import AlectryonTransform
-   AlectryonTransform.SERTOP_ARGS = ["-Q", "/coq/source/path/,LibraryName"]
+   AlectryonTransform.DRIVER_ARGS["sertop"] = ["-Q", "/coq/source/path/,LibraryName"]
 
-Note that the syntax of ``SERTOP_ARGS`` is the one of ``sertop``, not the one of
+Note that the syntax of ``DRIVER_ARGS["sertop"]`` is the one of ``sertop``, not the one of
 ``coqc`` (/~https://github.com/ejgallego/coq-serapi/issues/215).
 
 Adding custom keywords

alectryon/cli.py

@@ -61,22 +61,22 @@ def rst_to_coq(coq, fpath, point, marker):
     return _catch_parsing_errors(fpath, rst2coq_marked, coq, point, marker)
 
 def annotate_chunks(chunks, fpath, cache_directory, cache_compression,
-                    sertop_args, exit_code):
-    from .serapi import SerAPI
+                    input_language, driver_name, driver_args, exit_code):
     from .core import StderrObserver
     from .json import Cache
-    api = SerAPI(sertop_args, fpath=fpath)
-    metadata = {"sertop_args": sertop_args}
-    cache = Cache(cache_directory, fpath, metadata, cache_compression)
-    annotated = cache.update(chunks, api.annotate, SerAPI.version_info())
-    assert isinstance(api.observer, StderrObserver)
-    exit_code.val = int(api.observer.exit_code >= 3)
+    driver_cls = core.resolve_driver(input_language, driver_name)
+    driver = driver_cls(driver_args, fpath=fpath)
+    cache = Cache(cache_directory, fpath, driver.metadata, cache_compression)
+    annotated = cache.update(chunks, driver.annotate, driver.version_info())
+    assert isinstance(driver.observer, StderrObserver)
+    exit_code.val = int(driver.observer.exit_code >= 3)
     return annotated
 
 def register_docutils(v, ctx):
     from . import docutils
 
-    docutils.AlectryonTransform.SERTOP_ARGS = ctx["sertop_args"]
+    docutils.AlectryonTransform.DRIVER_ARGS = ctx["driver_args_by_name"]
+    docutils.AlectryonTransform.LANGUAGE_DRIVERS = ctx["language_drivers"]
     docutils.CACHE_DIRECTORY = ctx["cache_directory"]
     docutils.CACHE_COMPRESSION = ctx["cache_compression"]
     docutils.HTML_MINIFICATION = ctx["html_minification"]
@@ -285,11 +285,10 @@ def copy_assets(state, assets: List[Tuple[str, Union[str, core.Asset]]],
 
 def dump_html_standalone(snippets, fname, webpage_style,
                          html_minification, include_banner, include_vernums,
-                         assets, html_classes):
+                         assets, html_classes, input_language, driver_name):
     from dominate import tags, document
     from dominate.util import raw
     from . import GENERATOR
-    from .serapi import SerAPI
     from .html import ASSETS, ADDITIONAL_HEADS, JS_UNMINIFY, gen_banner, wrap_classes
 
     doc = document(title=fname)
@@ -319,7 +318,8 @@ def dump_html_standalone(snippets, fname, webpage_style,
     cls = wrap_classes(webpage_style, *html_classes)
     root = doc.body.add(tags.article(cls=cls))
     if include_banner:
-        root.add(raw(gen_banner(SerAPI.version_info(), include_vernums)))
+        driver = core.resolve_driver(input_language, driver_name)
+        root.add(raw(gen_banner(driver.version_info(), include_vernums)))
     for snippet in snippets:
         root.add(snippet)
 
@@ -475,6 +475,13 @@ def write_file(ext):
     'md': 'webpage',
 }
 
+INPUT_LANGUAGE = {
+    "coq": "coq",
+    "coqdoc": "coq",
+    "coq+rst": "coq",
+    "json": "coq",
+}
+
 def infer_mode(fpath, kind, arg, table):
     for (ext, mode) in table:
         if fpath.endswith(ext):
@@ -525,12 +532,25 @@ def post_process_arguments(parser, args):
         "latex": args.latex_dialect
     }
 
+    args.language_drivers = {
+        "coq": args.coq_driver
+    }
+
+    coq_args = []
     for (dirpath,) in args.coq_args_I:
-        args.sertop_args.extend(("-I", dirpath))
+        coq_args.extend(("-I", dirpath))
     for pair in args.coq_args_R:
-        args.sertop_args.extend(("-R", ",".join(pair)))
+        coq_args.extend(("-R", ",".join(pair)))
     for pair in args.coq_args_Q:
-        args.sertop_args.extend(("-Q", ",".join(pair)))
+        coq_args.extend(("-Q", ",".join(pair)))
+
+    args.sertop_args.extend(coq_args)
+    args.coqc_args.extend(coq_args)
+
+    args.driver_args_by_name = {
+        "sertop": args.sertop_args,
+        "coqc_time": args.coqc_args,
+    }
 
     # argparse applies ‘type’ before ‘choices’, so we do the conversion here
     args.copy_fn = COPY_FUNCTIONS[args.copy_fn]
@@ -580,6 +600,11 @@ def build_parser():
     in_.add_argument("--frontend", default=None, choices=FRONTEND_CHOICES,
                      help=FRONTEND_HELP)
 
+    COQ_DRIVER_HELP = "Choose which driver to use to execute Coq proofs."
+    COQ_DRIVER_CHOICES = sorted(core.DRIVERS_BY_LANGUAGE["coq"])
+    in_.add_argument("--coq-driver", default="sertop",
+                     choices=COQ_DRIVER_CHOICES,
+                     help=COQ_DRIVER_HELP)
 
     out = parser.add_argument_group("Output configuration")
 
@@ -670,12 +695,20 @@ def build_parser():
 
     subp = parser.add_argument_group("SerAPI process configuration")
 
-    SERTOP_ARGS_HELP = "Pass a single argument to SerAPI (e.g. -Q dir,lib)."
+    SERTOP_ARGS_HELP = ("Pass a single argument to SerAPI "
+                        "(e.g. --sertop-arg=-Q --sertop-arg=dir,lib).")
     subp.add_argument("--sertop-arg", dest="sertop_args",
                       action="append", default=[],
-                      metavar="SERAPI_ARG",
+                      metavar="SERTOP_ARG",
                       help=SERTOP_ARGS_HELP)
 
+    COQC_ARGS_HELP = ("Pass a single argument to coqc "
+                        "(e.g. --coqc-arg=-noinit).")
+    subp.add_argument("--coqc-arg", dest="coqc_args",
+                      action="append", default=[],
+                      metavar="SERAPI_ARG",
+                      help=COQC_ARGS_HELP)
+
     I_HELP = "Pass -I DIR to the SerAPI subprocess."
     subp.add_argument("-I", "--ml-include-path", dest="coq_args_I",
                       metavar="DIR", nargs=1, action="append",
@@ -738,10 +771,16 @@ def build_context(fpath, args, frontend, backend):
 
     dialect = args.backend_dialects.get(backend)
 
+    # These may be none (e.g. in reST mode)
+    input_language = INPUT_LANGUAGE.get(frontend)
+    driver_name = args.language_drivers.get(input_language)
+    driver_args = args.driver_args_by_name.get(driver_name, ())
+
     ctx = {**vars(args),
            "fpath": fpath, "fname": fname, "input_is_stdin": input_is_stdin,
            "frontend": frontend, "backend": backend, "dialect": dialect,
-           "input_language": "coq",
+           "input_language": input_language,
+           "driver_name": driver_name, "driver_args": driver_args,
            "assets": [], "html_classes": [], "exit_code": ExitCode(0)}
     ctx["ctx"] = ctx
 
@@ -800,19 +839,19 @@ def main():
 def rstcoq2html():
     """Docutils entry point for Coq → HTML conversion."""
     DESCRIPTION = 'Build an HTML document from an Alectryon Coq file.'
-    return _docutils_cmdline(DESCRIPTION, "coq+rst", "webpage")
+    return _docutils_cmdline(DESCRIPTION, "coq+rst", "webpage", "html4")
 
 def coqrst2html():
     """Docutils entry point for reST → HTML conversion."""
     DESCRIPTION = 'Build an HTML document from an Alectryon reStructuredText file.'
-    return _docutils_cmdline(DESCRIPTION, "rst", "webpage")
+    return _docutils_cmdline(DESCRIPTION, "rst", "webpage", "html4")
 
 def rstcoq2latex():
     """Docutils entry point for Coq → LaTeX conversion."""
     DESCRIPTION = 'Build a LaTeX document from an Alectryon Coq file.'
-    return _docutils_cmdline(DESCRIPTION, "coq+rst", "latex")
+    return _docutils_cmdline(DESCRIPTION, "coq+rst", "latex", "pdflatex")
 
 def coqrst2latex():
     """Docutils entry point for reST → LaTeX conversion."""
     DESCRIPTION = 'Build a LaTeX document from an Alectryon reStructuredText file.'
-    return _docutils_cmdline(DESCRIPTION, "rst", "latex")
+    return _docutils_cmdline(DESCRIPTION, "rst", "latex", "pdflatex")

alectryon/core.py

@@ -22,6 +22,7 @@
 
 from collections import namedtuple, defaultdict
 from contextlib import contextmanager
+from importlib import import_module
 from pathlib import Path
 from shlex import quote
 from shutil import which
@@ -279,6 +280,10 @@ def version_info(cls, binpath=None):
         bs = check_output([cls.resolve_driver(binpath or cls.BIN), *cls.VERSION_FLAGS])
         return GeneratorInfo(cls.NAME, bs.decode('ascii', 'ignore').strip())
 
+    @property
+    def metadata(self):
+        return {"args": self.user_args}
+
     @classmethod
     def driver_not_found(cls, binpath) -> NoReturn:
         """Raise an error to indicate that ``binpath`` cannot be found."""
@@ -333,3 +338,20 @@ def kill(self):
     def reset(self):
         """Start or restart this proper instance."""
         self.repl = self.start(stderr=sys.stderr)
+
+DRIVERS_BY_LANGUAGE = {
+    "coq": {
+        "sertop": (".serapi", "SerAPI"),
+        "coqc_time": (".coqc_time", "CoqcTime"),
+    }
+}
+
+def resolve_driver(input_language, driver_name):
+    if input_language not in DRIVERS_BY_LANGUAGE:
+        raise ValueError("Unknown language: {}".format(input_language))
+    known_drivers = DRIVERS_BY_LANGUAGE[input_language]
+    if driver_name not in known_drivers:
+        MSG = "Unknown driver for language {}: {}"
+        raise ValueError(MSG.format(input_language, driver_name))
+    mod, cls = known_drivers[driver_name]
+    return getattr(import_module(mod, __package__), cls)

alectryon/docutils.py

@@ -66,7 +66,7 @@
 side, and a doctree-resolved event on the Sphinx side.
 """
 
-from typing import Any, Dict, List, Optional
+from typing import Any, Dict, List, Optional, Iterable, DefaultDict
 
 import re
 import os.path
@@ -90,7 +90,6 @@
 
 from . import core, transforms, html, latex, markers
 from .core import Gensym, Position, PosStr
-from .serapi import annotate, SerAPI
 from .pygments import make_highlighter, added_tokens, validate_style, \
     get_lexer, resolve_token, replace_builtin_coq_lexer
 
@@ -206,7 +205,11 @@ def _gensym_stem(document, suffix=""):
 class Config:
     def __init__(self, document):
         self.tokens = {}
-        self.sertop_args = []
+        self.language_drivers = AlectryonTransform.LANGUAGE_DRIVERS.copy()
+        self.driver_args: DefaultDict[str, List[str]] = defaultdict(list)
+        for nm, args in AlectryonTransform.DRIVER_ARGS.items():
+            self.driver_args[nm] = list(args)
+        self.driver_args["sertop"].extend(AlectryonTransform.SERTOP_ARGS)
         self.document = document
         self.read_docinfo()
 
@@ -247,7 +250,7 @@ def parse_docinfo_field(self, node, name, body):
             self.tokens.setdefault(token, []).extend(body.split())
         elif name == "alectryon/serapi/args":
             import shlex
-            self.sertop_args.extend(self.parse_args(shlex.split(body)))
+            self.driver_args["sertop"].extend(self.parse_args(shlex.split(body)))
         else:
             return
         node.parent.remove(node)
@@ -267,6 +270,13 @@ def parse_args(args):
                 yield "-" + arg
                 yield ",".join(vals)
 
+    def driver_info(self, lang):
+        driver_name = self.language_drivers[lang]
+        driver_cls = core.resolve_driver(lang, driver_name)
+        driver_args = self.driver_args[driver_name]
+        assert driver_name == driver_cls.ID
+        return driver_cls, driver_args
+
 class OneTimeTransform(Transform):
     def _apply(self):
         raise NotImplementedError()
@@ -327,7 +337,10 @@ class AlectryonTransform(OneTimeTransform):
     auto_toggle = True
 
     SERTOP_ARGS = ()
-    """Arguments to pass to SerAPI, in SerAPI format."""
+    """Arguments to pass to SerAPI, in SerAPI format (deprecated)."""
+
+    LANGUAGE_DRIVERS: Dict[str, str] = {"coq": "sertop"}
+    DRIVER_ARGS: Dict[str, Iterable[str]] = {"sertop": (), "coqc_time": ()}
 
     def check_for_long_lines(self, node, fragments):
         if LONG_LINE_THRESHOLD is None:
@@ -340,22 +353,20 @@ def check_for_long_lines(self, node, fragments):
             # remove the node created by ``Reporter.system_message``:
             self.document.transform_messages.remove(w)
 
-    def annotate_cached(self, chunks, sertop_args):
+    def annotate_cached(self, chunks, driver_cls, driver_args):
         from .json import Cache
         docpath = self.document['source']
-        # Later: decouple from SerAPI by generalizing over `annotate`
-        prover = SerAPI(sertop_args, fpath=docpath)
-        prover.observer = DocutilsObserver(self.document)
-        metadata = {"sertop_args": sertop_args}
-        cache = Cache(CACHE_DIRECTORY, docpath, metadata, CACHE_COMPRESSION)
-        annotated = cache.update(chunks, prover.annotate, prover.version_info())
+        driver = driver_cls(driver_args, fpath=docpath)
+        driver.observer = DocutilsObserver(self.document)
+        cache = Cache(CACHE_DIRECTORY, docpath, driver.metadata, CACHE_COMPRESSION)
+        annotated = cache.update(chunks, driver.annotate, driver.version_info())
         return cache.generator, annotated
 
     def annotate(self, pending_nodes):
         config = alectryon_state(self.document).config
-        sertop_args = (*self.SERTOP_ARGS, *config.sertop_args)
         chunks = [pending.details["contents"] for pending in pending_nodes]
-        return self.annotate_cached(chunks, sertop_args)
+        driver_cls, driver_args = config.driver_info("coq")
+        return self.annotate_cached(chunks, driver_cls, driver_args)
 
     def replace_node(self, pending, fragments):
         directive_annots = pending.details["directive_annots"]

alectryon/serapi.py

@@ -80,6 +80,10 @@ def driver_not_found(cls, binpath):
     def topfile(self):
         return CoqIdents.topfile_of_fpath(self.fpath)
 
+    @property
+    def metadata(self):
+        return {"sertop_args": self.user_args}
+
     def _next_sexp(self):
         """Wait for the next sertop prompt, and return the output preceding it."""
         response = self._read()