↓Skip to main content
IT Blog IT Blog
  1. All Posts/

alectryon

Tools HTML

Alectryon

A library to process Coq and Lean 4 snippets embedded in text documents, showing goals and messages for each input sentence. Also a literate programming toolkit. The goal of Alectryon is to make it easy to write textbooks, blog posts, and other documents that mix interactive proofs and prose.

Alectryon is typically used in one of three ways:

  • As a library, through its Python API
  • As a Docutils/Sphinx extension, allowing you to include annotated snippets into your reStructuredText and Markdown documents. During compilation, Alectryon collects all .. coq:: code blocks, feeds their contents to Coq, and incorporates the resulting goals and responses into the final document.
  • As a standalone compiler, allowing you to include prose delimited by special (*"https://github.com/cpitclaudel/…"*) comments directly into your Coq source files (in the style of coqdoc). When invoked, Alectryon translates your Coq file into a reStructuredText document and compiles it using the standard reStructuredText toolchain.

For background information, check out the quickstart guide on the MIT PLV blog, the SLE2020 paper (open access) and its live examples, or the conference talk.
Alectryon is free software under a very permissive license. If you use it, please remember to cite it, and please let me know!
Some examples of use in the wild are linked at the bottom of this page. Please add your own work by submitting a PR!

Setup

To install from OPAM and PyPI:

opam install "coq-serapi>=8.10.0+0.7.0" (from the Coq OPAM archive)
python3 -m pip install alectryon

To install the latest version from Git, use python3 -m pip install git+https://github.com/cpitclaudel/alectryon.git. To install from a local clone, use python3 -m pip install ..
A note on dependencies: the serapi module only depends on the coq-serapi OPAM package. dominate is used in alectryon.html to generate HTML output, and pygments is used by the command-line application for syntax highlighting. reStructuredText support requires docutils (and optionally sphinx); Markdown support requires myst_parser (docs); Coqdoc support requires beautifulsoup4. Support for Coq versions follows SerAPI; Coq ≥ 8.10 works well and ≥ 8.12 works best.

Usage

As a standalone program

Recipes

Try these recipes in the recipes directory of this repository (for each task I listed two commands: a short one and a longer one making everything explicit):
Generate an interactive webpage from a literate Coq file with reST comments (Coqdoc style):

alectryon literate_coq.v
alectryon --frontend coq+rst --backend webpage literate_coq.v -o literate_coq.html

Generate an interactive webpage from a plain Coq file (Proof General style):

alectryon --frontend coq plain.v
alectryon --frontend coq --backend webpage plain.v -o plain.v.html

Generate an interactive webpage from a Coqdoc file (compatibility mode):

alectryon --frontend coqdoc coqdoc.v
alectryon --frontend coqdoc --backend webpage coqdoc.v -o coqdoc.html

Generate an interactive webpage from a reStructuredText document containing .. coq:: directives (coqrst style):

alectryon literate_reST.rst
alectryon --frontend rst --backend webpage literate_reST.rst -o literate_reST.html

Generate an interactive webpage from a Markdown document written in the MyST dialect, containing .. coq:: directives:

alectryon literate_MyST.md
alectryon --frontend md --backend webpage literate_MyST.md -o literate_MyST.html

Translate a reStructuredText document into a literate Coq file:

alectryon literate_reST.rst -o literate_reST.v
alectryon --frontend rst --backend coq+rst literate_reST.rst -o literate_reST.v

Translate a literate Coq file into a reStructuredText document:

alectryon literate_coq.v -o literate_coq.v.rst
alectryon --frontend coq+rst --backend rst literate_coq.v -o literate_coq.v.rst

Record goals and responses for fragments contained in a JSON source file:

alectryon fragments.v.json
alectryon --frontend coq.json --backend json fragments.json -o fragments.v.io.json

Record goals and responses and format them as HTML for fragments contained in a JSON source file:

alectryon fragments.v.json -o fragments.v.snippets.html
alectryon --frontend coq.json --backend snippets-html fragments.json -o fragments.v.snippets.html

Command-line interface 

alectryon [-h] […]
          [--frontend {coq,coq+rst,coqdoc,json,md,rst}]
          [--backend {coq,coq+rst,json,latex,rst,snippets-html,snippets-latex,webpage,…}]
          input [input ...]

Use alectryon --help for full command line details.

  • Each input file can be .v (a Coq source file, optionally including reStructuredText in comments delimited by (*"https://github.com/cpitclaudel/…"*)), .json (a list of Coq fragments), .rst (a reStructuredText document including .. coq:: code blocks), or .md (a Markdown/MyST document including {coq} code blocks). Each input fragment is split into individual sentences, which are executed one by one (all code is run in a single Coq session).
  • One output file is written per input file. Each frontend supports a subset of all backends.

    • With --backend webpage (the default for most inputs), output is written as a standalone webpage named <input>.html (for coq+rst inputs) or <input>.v.html (for plain coq inputs).
    • With --backend snippets-html, output is written to <input>.snippets.html as a sequence of <pre class="alectryon-io"> blocks, separated by <!-- alectryon-block-end --> markers (there will be as many blocks as entries in the input list if input is a .json file).
    • With --backend json, output is written to <input>.io.json as a JSON-encoded list of Coq fragments (as many as in input if input is a .json file). Each fragment is a list of records, each with a _type and some type-specific fields. Here is an example:

      Input (minimal.json): 

          <pre>["Example xyz (H: False): True. (* ... *) exact I. Qed.",

      “Print xyz.”]

          <p>
      Output (<code>minimal.json.io.json</code>) after running <code>alectryon --writer json minimal.json</code>:
    </p>
    
    <pre>[ // A list of processed fragments

      [ // Each fragment is a list of records { // Each record has a type, and type-specific fields “_type”: “sentence”, “sentence”: “Example xyz (H: False): True.”, “responses”: [], “goals”: [ { “_type”: “goal”, “name”: “2”, “conclusion”: “True”, “hypotheses”: [ { “_type”: “hypothesis”, “name”: “H”, “body”: null, “type”: “False” } ] } ] }, {"_type": “text”, “string”: " (* … *) “}, {"_type”: “sentence”, “sentence”: “exact I.”, “responses”: [], “goals”: []}, {"_type": “text”, “string”: " “}, {"_type”: “sentence”, “sentence”: “Qed.”, “responses”: [], “goals”: []} ], [ // This is the second fragment { “_type”: “sentence”, “sentence”: “Print xyz.”, “responses”: [“xyz = fun _ : False => In : False -> True”], “goals”: [] } ] ]

  • The exit code produced by Alectryon indicates whether the conversion succeeded: for success, 1 for a generic error, and 10 + the level of the most severe Docutils error if using a Docutils-based pipeline (hence 10 is debug, 11 is info, 12 is warning, 13 is error, and 14 is severe error). Docutils errors at levels below exit_status_level (default: 3) do not affect the exit code, so level 10, 11, and 12 are not used by default.

As a library

Use alectryon.serapi.annotate(chunks: List[str]), which returns an object with the same structure as the JSON above, but using objects instead of records with a _type field:

>>> from alectryon.serapi import annotate
>>> annotate(["Example xyz (H: False): True. (* ... *) exact I. Qed.", "Check xyz."])
[# A list of processed fragments
 [# Each fragment is a list of records (each an instance of a namedtuple)
  Sentence(contents='Example xyz (H: False): True.',
           messages=[],
           goals=[Goal(name=None,
                      ...


↑