Untangling mechanized proofs

An introduction to Alectryon

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming.

Coq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like CoqIDE or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Coq is to manually copy Coq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Coq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Coq IDE for writing proofs.

I have a talk about this at SLE2020 on November 16th; you should join!

Below, you can see three examples: in the first one I asked Alectryon to record the result of a single Check command. In the second, I recorded an error message printed by Coq. In the third, I recorded a simple proof script — try hovering or clicking on Coq sentences. In the last, I've used hidden Show Proof commands to show how each tactic participates in constructing a proof term.

Check bool_ind.bool_ind
     : forall P : bool -> Prop,
       P true -> P false -> forall b : bool, P b

Check (1 + true).The term "true" has type "bool"
while it is expected to have type "nat".

Lemma rev_rev {A} (l: list A) :
  List.rev (List.rev l) = l.A: Type
l: list A
rev (rev l) = l
Proof.A: Type
l: list A
rev (rev l) = l
  induction l.A: Type
rev (rev nil) = nil
A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev (a :: l)) = a :: l
  - (* l ← [] *)A: Type
rev (rev nil) = nil
    cbn.A: Type
nil = nil reflexivity.
  - (* l ← _ :: _ *)A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev (a :: l)) = a :: l
    cbn.A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (rev l ++ a :: nil) = a :: l
    rewrite rev_app_distr.A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (a :: nil) ++ rev (rev l) = a :: l
    rewrite IHl.A: Type
a: A
l: list A
IHl: rev (rev l) = l
rev (a :: nil) ++ l = a :: l
    cbn.A: Type
a: A
l: list A
IHl: rev (rev l) = l
a :: l = a :: l reflexivity.
Qed.

Context (classical: forall A, A \/ ~ A).
Example double_negation : (forall A, ~~A -> A).classical: forall A : Prop, A \/ ~ A
forall A : Prop, ~ ~ A -> A
Proof.classical: forall A : Prop, A \/ ~ A
forall A : Prop, ~ ~ A -> A
  intros A notnot_A.classical: forall A0 : Prop, A0 \/ ~ A0
A: Prop
notnot_A: ~ ~ A
A
(fun (A : Prop) (notnot_A : ~ ~ A) => ?Goal)  destruct (classical A) as [_A | not_A].classical: forall A0 : Prop, A0 \/ ~ A0
A: Prop
notnot_A: ~ ~ A
_A: A
A
classical: forall A0 : Prop, A0 \/ ~ A0
A: Prop
notnot_A: ~ ~ A
not_A: ~ A
A
(fun (A : Prop) (notnot_A : ~ ~ A) =>
 let o : A \/ ~ A := classical A in
 match o with
 | or_introl _A => ?Goal
 | or_intror not_A => ?Goal0
 end)  - (* A holds *)classical: forall A0 : Prop, A0 \/ ~ A0
A: Prop
notnot_A: ~ ~ A
_A: A
A
    assumption.
(fun (A : Prop) (notnot_A : ~ ~ A) =>
 let o : A \/ ~ A := classical A in
 match o with
 | or_introl _A => _A
 | or_intror not_A => ?Goal
 end)  - (* A does not hold *)classical: forall A0 : Prop, A0 \/ ~ A0
A: Prop
notnot_A: ~ ~ A
not_A: ~ A
A
    elim (notnot_A not_A).
(fun (A : Prop) (notnot_A : ~ ~ A) =>
 let o : A \/ ~ A := classical A in
 match o with
 | or_introl _A => _A
 | or_intror not_A => False_ind A (notnot_A not_A)
 end)Qed.

By the way, I wrote an academic paper at SLE2020 on Alectryon. It has plenty of cool visualizations and examples, it goes into much more depth than this intro, and importantly it has all the related work, including lots of stuff on procedural vs declarative proofs. This blog post, the paper, and the talk were all built with Alectryon.

If this is your first time on this blog, you might want to check the very short tutorial on navigating these visualizations before proceeding with the rest of this post.

A quick tour of Alectryon

The library was written with two scenarios in mind:

Making it easier to browse Coq developments (even if these developments are not written in literate style) by turning Coq source files into webpages allowing readers to replay proofs in their browser (the “Proviola” style). As a demo, I recorded goals and responses for a complete build of the Flocq library.
Writing documents mixing Coq source code and explanatory prose, either starting from a text file containing special directives (the “coqtex” and “coqrst” style, used in Coq's reference manual), or starting from a Coq file containing special comments (the “coqdoc” style, used in CPDT, Software foundations, etc.).

The Alectryon paper, this blog post, and my SLE talk are examples of the former (they are written in reStructuredText, a Markdown-like markup language); as another example, here is a chapter from FRAP and one from CPDT, converted to reStructuredText by hand (change the URLs to .rst to see the sources).

As a demo of the latter here's a full build of Logical Foundations.

There's no support for attaching bits of documentation to specific bits of code, like definitions, axioms, variables, etc. As I've written in the past, I think this is a different job (“docstrings”), ideally to be handled by Coq itself (similar to how it tracks the body and location of definitions). Alectryon also doesn't support hyperlink Coq terms to their definitions like coqdoc can, but I plan to implement this eventually.

Generating webpages

Alectryon's main purpose is to record Coq's outputs and interleave them with the corresponding inputs to create an interactive webpage:

Theorem rev_length : ∀ l : list nat,
    length (rev l) = length l.∀ l : list nat, length (rev l) = length l
Proof.∀ l : list nat, length (rev l) = length l
  intros l.l: list nat
length (rev l) = length l
  induction l as [| n l' IHl'].length (rev nil) = length nil
n: nat
l': list nat
IHl': length (rev l') = length l'
length (rev (n :: l')) = length (n :: l')
  - (* l ← [] *)length (rev nil) = length nil
    reflexivity.
  - (* l ← _ :: _ *)n: nat
l': list nat
IHl': length (rev l') = length l'
length (rev (n :: l')) = length (n :: l')
    simpl.n: nat
l': list nat
IHl': length (rev l') = length l'
length (rev l' ++ n :: nil) = S (length l')
    rewrite app_length.n: nat
l': list nat
IHl': length (rev l') = length l'
length (rev l') + length (n :: nil) = S (length l')
    rewrite Nat.add_comm.n: nat
l': list nat
IHl': length (rev l') = length l'
length (n :: nil) + length (rev l') = S (length l')
    simpl.n: nat
l': list nat
IHl': length (rev l') = length l'
S (length (rev l')) = S (length l')
    rewrite IHl'.n: nat
l': list nat
IHl': length (rev l') = length l'
S (length l') = S (length l')
    reflexivity.
Qed.

Check rev_length.rev_length
     : ∀ l : list nat, length (rev l) = length l

Because this is an interactive webpage, we can apply all sorts of post-processing to the output, like using MathJax to make a math proof a bit more readable:

Lemma Gauss: ∀ n, 2 * (nsum n (fun i => i)) = n * (n + 1).\ccForall{n : \ccNat{}}{2 \times \ccNsum{i}{n}{i} =
                        n \times (n + 1)}
Proof.\ccForall{n : \ccNat{}}{2 \times \ccNsum{i}{n}{i} =
                        n \times (n + 1)}
  induction n; cbn [nsum].2 \times 0 = 0 \times (0 + 1)
n: \ccNat{}
IHn: 2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
  - (* n ← 0 *)2 \times 0 = 0 \times (0 + 1)
    reflexivity.
  - (* n ← S _ *)n: \ccNat{}
IHn: 2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite Mult.mult_plus_distr_l.2 \times \ccSucc{ n} + 2 \times \ccNsum{i}{n}{i} =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite IHn.2 \times \ccSucc{ n} + n \times (n + 1) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    ring.
Qed.

… or using the browser's native support for vector graphics to render Game of Life boards encoded as lists of Booleans into small images:

Definition glider := [[0;1;0;0;0];
                      [0;0;1;0;0];
                      [1;1;1;0;0];
                      [0;0;0;0;0];
                      [0;0;0;0;0]].
Compute take 9 (iter conway_life glider).= [[[0; 1; 0; 0; 0]; [0; 0; 1; 0; 0];
   [1; 1; 1; 0; 0]; [0; 0; 0; 0; 0];
   [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [1; 0; 1; 0; 0];
  [0; 1; 1; 0; 0]; [0; 1; 0; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 1; 0; 0];
  [1; 0; 1; 0; 0]; [0; 1; 1; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 1; 0; 0; 0];
  [0; 0; 1; 1; 0]; [0; 1; 1; 0; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 1; 0; 0];
  [0; 0; 0; 1; 0]; [0; 1; 1; 1; 0];
  [0; 0; 0; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 1; 0; 1; 0]; [0; 0; 1; 1; 0];
  [0; 0; 1; 0; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 0; 1; 0]; [0; 1; 0; 1; 0];
  [0; 0; 1; 1; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 1; 0; 0]; [0; 0; 0; 1; 1];
  [0; 0; 1; 1; 0]];
  [[0; 0; 0; 0; 0]; [0; 0; 0; 0; 0];
  [0; 0; 0; 1; 0]; [0; 0; 0; 0; 1];
  [0; 0; 1; 1; 1]]]
: list (list (list bool))

… or using a graph library to draw visualizations that makes it clearer what happens when one builds a red-black tree with Coq.MSets.MSetRBT.

Module RBT := MSets.MSetRBT.Make Nat_as_OT.

Definition build_trees (leaves: list nat) :=
  List.fold_left (fun trs n =>
        RBT.add n (hd RBT.empty trs) :: trs)
    leaves [] |> List.rev.

Compute build_trees [1;2;3;4;5].= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '2'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '5'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}]
: list RBT.t
Compute build_trees [2;1;4;3;6].= [{ 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } }};
  { 'tree': { 'kind':'node'; 'color': 'Black'; 'value': '3'; 'left': { 'kind':'node'; 'color': 'Black'; 'value': '2'; 'left': { 'kind':'node'; 'color': 'Red'; 'value': '1'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind': 'leaf' } }; 'right': { 'kind':'node'; 'color': 'Black'; 'value': '4'; 'left': { 'kind': 'leaf' }; 'right': { 'kind':'node'; 'color': 'Red'; 'value': '6'; 'left': { 'kind': 'leaf' }; 'right': { 'kind': 'leaf' } } } }}]
: list RBT.t

Do these visualizations really help? You be the judge: here's how the red-black tree example looks with plain-text output:

Compute build_trees [1;2;3;4;5].= [Node Black Leaf 1 Leaf;
  Node Black Leaf 1 (Node Red Leaf 2 Leaf);
  Node Black (Node Black Leaf 1 Leaf) 2
    (Node Black Leaf 3 Leaf);
  Node Black (Node Black Leaf 1 Leaf) 2
    (Node Black Leaf 3 (Node Red Leaf 4 Leaf));
  Node Black (Node Black Leaf 1 Leaf) 2
    (Node Red (Node Black Leaf 3 Leaf) 4
       (Node Black Leaf 5 Leaf))]
: list t
Compute build_trees [2;1;4;3;6].= [Node Black Leaf 2 Leaf;
  Node Black (Node Red Leaf 1 Leaf) 2 Leaf;
  Node Black (Node Red Leaf 1 Leaf) 2
    (Node Red Leaf 4 Leaf);
  Node Black
    (Node Black (Node Red Leaf 1 Leaf) 2 Leaf) 3
    (Node Black Leaf 4 Leaf);
  Node Black
    (Node Black (Node Red Leaf 1 Leaf) 2 Leaf) 3
    (Node Black Leaf 4 (Node Red Leaf 6 Leaf))]
: list t

Even if you don't use Alectryon's literate programming features, these webpages have one additional advantage beyond convenient browsing: because they record both your code and Coq's responses, they can serve as a permanent record of your developments immune to bitrot and suitable for archival.

Editing literate Coq documents

Besides generating webpages from standalone Coq files, Alectryon can help you write documentation, blog posts, and all sorts of other documents mixing proofs and prose. Alectryon's literate module implements translations from Coq to reStructuredText and from reStructuredText to Coq, which allow you to toggle between two independent views of the same document: one best for editing code, and one best for editing reST prose. Concretely, Alectryon knows how to convert between this:

=============================
 Writing decision procedures
=============================

Here's an inductive type:

.. coq::

   Inductive Even : nat -> Prop :=
   | EvenO : Even O
   | EvenS : forall n, Even n -> Even (S (S n)).

.. note::

   It has two constructors:

   .. coq:: unfold out

      Check EvenO.
      Check EvenS.

… and this:

(*|
=============================
 Writing decision procedures
=============================

Here's an inductive type:
|*)

Inductive Even : nat -> Prop :=
| EvenO : Even O
| EvenS : forall n, Even n -> Even (S (S n)).

(*|
.. note::

   It has two constructors:
|*)

Check EvenO.
Check EvenS.

Because the transformations are (essentially) inverses of each other, you don't have to pick one of these two styles and stick to it (or worse, to maintain two copies of the same document, copy-pasting snippets back and forth). Instead, you can freely switch between using your favorite Coq IDE to write code and proofs while editing bits of prose within comments, and using your favorite reStructuredText editor to write prose.

The reason for picking reStructuredText as the markup language for comments is that it's designed with extensibility in mind, which allows me to plug Alectryon into the standard Docutils and Sphinx compilation pipelines for reStructuredText (Sphinx is what the documentations of Haskell, Agda, Coq, and Python are written in). This is how this blog is written, and in fact you can download the sources if you're curious to see what it looks like. This is also how I made my SLE2020 slides (press p to see the presenter notes) and how I wrote my SLE2020 paper.

A small Emacs package (alectryon.el), allows you to toggle quickly between Coq and reST. The screenshot below demonstrates this feature: on the left is the Coq view of an edited excerpt of Software Foundations, in coq-mode; on the right is the reST view of the same excerpt, in a rst-mode buffer. The conversion is transparent, so editing either view updates the same .v file on disk. Notice the highlight indicating a reStructuredText warning on both sides:

Side-by-side comparisons of Coq and reStructuredText views of the same document

Alectryon's syntax-highlighting is done with Pygments, but it uses an update Coq grammar with a database of keywords and commands extracted directly from the reference manual (ultimately, this part should be merged upstream, and the database-generation tool should be merged into the Coq reference manual; I'll write a separate blog post about it at some point).

Recording Coq's output and caching it

Alectryon's design is pretty modular, so if you want to use it for other purposes it's easy to use just some parts of it. In particular, its core is a simple API that takes a list of code snippets, feeds them to Coq through SerAPI, and records goals and messages. This functionality is exposed on the command line (taking json as input and producing json as output) and also as a Python module:

>>> from alectryon.core import annotate
>>> annotate(["Example xyz (H: False): True. (* ... *) exact I. Qed.", "Print xyz."])
[[CoqSentence(
     sentence='Example xyz (H: False): True.',
     responses=[],
     goals=[CoqGoal(name='2',
                    conclusion='True',
                    hypotheses=[CoqHypothesis(name='H', body=None, type='False')])]),
  CoqText(string=' (* ... *) '),
  CoqSentence(sentence='exact I.', responses=[], goals=[]),
  CoqText(string=' '),
  CoqSentence(sentence='Qed.', responses=[], goals=[])],

 [CoqSentence(sentence='Print xyz.',
              responses=['xyz = fun _ : False => I\n     : False -> True'],
          goals=[])]]

Alectryon uses JSON caches to speed up consecutive runs, but even when performance isn't a problem caches provide a very useful form of regression testing for embedded Coq snippets. Without such tests, it's easy for seemingly innocuous changes in a library to break its documentation in subtle ways. For example, you might have the following snippet:

The function plus is defined recursively:

Print plus.plus = 
fix plus (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (plus p m)
  end
     : nat → nat → nat

Argument scopes are [nat_scope nat_scope]

If you rename plus to Nat.add and add a compatibility notation, this is what your documentation will silently become, with no error or warning to let you realize that something went wrong:

Print plus.Notation plus := Init.Nat.add

This was such a common problem in the reference manual that we implemented workarounds to catch the most egregious cases (where changes caused snippets to print errors instead of executing successfully). But if you check in Alectryon's caches into source control, then the following will show up pretty clearly:

  "contents": "Print plus.",
  "messages": [
    {
      "_type": "message",
-     "contents": "plus = \nfix plus (n m : nat) {struct n} : nat := …"
+     "contents": "Notation plus := Nat.add"
    }

All these features are exposed through a command line interface documented in Alectryon's README. This project has been in development for over a year, but there's still lots of rough bits, so expect bugs and please report them!

Using Alectryon

Standalone usage

The easiest way to get started Alectryon is to use it very much like coqdoc, but using reStructuredText syntax in special comments delimited with (*| and |*), like in this hypothetical even.v document:

(*|
=======
 Title
=======

Prose. *Emphasis*; **strong emphasis**; ``code``; `coq code`; `link <url>`__.
|*)

Inductive Even : nat -> Prop :=
| EvenO : Even O
| EvenS : forall n, Even n -> Even (S (S n)).

… which can then be compiled into a static webpage using ../alectryon.py --frontend coq+rst --backend webpage even.v -o even.html.

This is what I did for FRAP and CPDT. For Software foundations and Flocq, I used a compatibility layer combining Alectryon to render the code and coqdoc to render the prose:

find . -name *.v -exec alectryon.py --frontend coqdoc --backend webpage {} \;

Authoring tips

There's a great reStructuredText primer on Sphinx's website, if you're new to this markup language (there's also an official quick-reference guide, which is as ugly as it is comprehensive). reStructuredText is no panacea, but it's a decent language with a good story about extensibility, and it's popular for writing documentation (Haskell, Agda, and Coq use it for their reference manuals).

If you use Emacs, you can install alectryon.el, a small Emacs library that makes it easy to toggle between reStructuredText and Coq:

(add-to-list 'load-path "path/to/alectryon/clone/")
(require 'alectryon)

With this, you'll get improved rendering of (*| … |*) comment markers, and you'll be able to toggle between reStructuredText and Coq with a simple press of C-c C-S-a. You probably also want to M-x package-install flycheck and pip3 install --user docutils, though neither of these are hard dependencies.

(Hi, reader! Are you thinking “why isn't this on MELPA?” Great question! It's because I haven't had the time to do it yet. But you can — yes, you! In exchange, I promise I'll sing your praises every time your name comes up in conversation — I might even refer to you as ‘writer-of-MELPA-recipes extraordinaire’.

Alternatively, if you're a member of this most distinguished category of people who write more grant proposals than Emacs Lisp programs, you should drop me a line: I'm on the academic job market this year, so we should chat!)

Integrated into a blog or manual

Alectryon is very easy to integrate with platforms and tools that support Sphinx or Docutils, like Pelican, readthedocs, Nikola, etc. (In the long run, I hope to migrate Coq's reference manual to Alectryon. It currently uses coqrst, a previous iteration of Alectryon that I wrote a few years ago based on coqtop instead of SerAPI).

For this blog, for example, I just added the following snippet to our pelicanconf.py:

import alectryon
import alectryon.docutils
from alectryon.html import ASSETS

# Register the ‘.. coq::’ directive
alectryon.docutils.register()

# Copy Alectryon's stylesheet
alectryon_assets = path.relpath(ASSETS.PATH, PATH)
STATIC_PATHS.append(alectryon_assets)
EXTRA_PATH_METADATA[alectryon_assets] = {'path': 'static/alectryon/'}

# Copy a custom Pygments theme with good contrast to theme/pygments
for pth in ("tango_subtle.css", "tango_subtle.min.css"):
    EXTRA_PATH_METADATA[path.join(alectryon_assets, pth)] = \
          {'path': path.join('theme/pygments/', pth)}

Similar steps would be needed for Sphinx, though using alectryon.sphinx.register() instead. I hear that there's work in progress to integrate with other blog platforms.

As a library

The choice of reStructuredText is a bit arbitrary, so it's not a hard dependency of Alectryon. It should be relatively straightforward to combine it with other input languages (like LaTeX, Markdown, etc.) — I just haven't found the time to do it. There's even an output mode that takes Coq fragments as input and produces individual HTML snippets for each, to make integration easier. See Alectryon's README for more info.

As an example, I made a compatibility shim for Coqdoc that uses Alectryon to render Coq code, responses, and goals, but calls to coqdoc to render the contents of (** … **) comments; look for coqdoc in file cli.py of the distribution to see how it works.

Some interesting technical bits

The vast majority of the processing time in Alectryon is spent parsing and unparsing s-expressions. I wrote Alectryon's s-exp parser myself to minimize dependencies and got it reasonably fast, but if you're a Python speed geek you should definitely have a look (I wonder if cython would help here — I'm not sure how good it is at bytestring manipulation). Hopefully this problem (and the corresponding code) will evaporate once SerAPI supports JSON.
The default HTML backend works without JavaScript — it uses only CSS. It stores its state in checkboxes: each input line is a label for a hidden checkbox, whose state controls the visibility of the output through conditional CSS rules. The document-wide toggle works the same way, overriding all individual checkboxes. You can see the page without the styles by typing javascript:document.querySelector("link[href$=\"alectryon.css\"]").remove() into your address bar (all responses, goals, and checkboxes will be displayed, and you'll lose the interactivity, of course).
Block comments in Coq are relatively complicated: parsers need to track not just nested comments but also nested strings, an oddity we inherited from OCaml (string delimiters in comments must be properly matched, and comment markers within them are ignored). The idea there was to make commenting more robust, so that wrapping a valid bit of code in (* … *) would always work. As an example, the following is valid OCaml code:
```
let a = "x *) y" in
(* let a = "x *) y" in *) a
```
… though as you may have guessed from the broken syntax highlighting, not many tools handle this properly — it will happily break Emacs' tuareg-mode, Pygments, etc.

But the whole point is moot in Coq, because *) is a fairly common token, and it's not disallowed (unlike in OCaml):
```
split; (try reflexivity; intros *).
```
Single-line comments solve this problem nicely. I've seen suggestions to use (*) in OCaml and Coq, but (1) it's quite unpleasant to type, (2) it'll break every editor that currently supports OCaml, and (3) it doesn't have natural variants ((* is a regular comment and (** is a coqdoc one; what would a literate variant of (*) be? Not (**), since that's the same as (* *))

Still, single-line comments would be nice. A few years ago I wrote a predecessor of Alectryon for F*, and using /// for literate comments makes it much easier to start new reST blocks, compared to relatively unwieldy (*| … |*) markers. As a bonus, the parsing/unparsing algorithms are a lot simpler (it turns out that (* and *) are pretty common token in reST as well, (like *this*), so Alectryon needs to do some quoting and unquoting instead of treating all text opaquely).
The conversion between Coq and reStructuredText keeps track of input positions and carries them throughout the translation, allowing it to annotate output lines with the input they came from. I use this when compiling from Coq+reST to HTML, to map reStructuredText error messages back to the original Coq sources. Additionally, if you have Flycheck installed, the alectryon.el Emacs mode uses that to lint the reStructuredText code embedded in Alectryon comments.

It actually took me a while to converge on a good design for this. One of the requirements is that the translator should be able to keep the position of at least one point, since we want to preserve the user's position in the document when we switch. With a rich string type this is trivial, but the string types in Python (and OCaml, and most languages really) are quite minimal. In Emacs Lisp, for example, we'd create a “point” marker, and convert the contents of the buffer from Coq to reST or vice-versa by making insertions and deletions into it, which would move the marker around automatically.

This would work in Python too, but it would be a lot of code to maintain for a single application (including reimplementing regex matching on top of this new structure), so instead I used a simpler type of strings annotated with position information only (in fact, for performance, these strings are just views over the original document, implemented as a string and a pair of offsets). Then I segment the original document into a collection of these views annotated with their kind (prose or code), slice and dice them further to add or remove indentation, ‘.. coq::’ markers, or comment delimiters, and finally assemble them into a Frankenstein monster of a document, composed of fragments from the original document pieced together by a few added strings (annoyingly, having to escape comment delimiters throws an extra complication, since there's no straightforward notion of replacement for these string views (instead, unescaping (\ * to produce (* requires splitting (* into three parts, dropping the middle one, and stitching the remaining two together).

The conversion from reST to Coq tries hard to keep as few .. coq:: directives as possible. For example:

reST	Coq
Some text .. coq:: Let a := 1. .. coq:: unfold Let b := 1. .. note:: More text. .. coq:: Let aa := 1. Final text. .. coq:: Let bb := 1.	(\| Some text \|) Let a := 1. (\| .. coq:: unfold \|) Let b := 1. (\| .. note:: More text. .. coq:: \|) Let aa := 1. (\| Final text. \|) Let bb := 1.

reST

Coq

Some text

.. coq::

   Let a := 1.

.. coq:: unfold

   Let b := 1.

.. note::

   More text.

.. coq::

   Let aa := 1.

Final text.

.. coq::

   Let bb := 1.

(*|
Some text
|*)

Let a := 1.

(*|
.. coq:: unfold
|*)

Let b := 1.

(*|
.. note::

   More text.

.. coq::
|*)

Let aa := 1.

(*|
Final text.
|*)

Let bb := 1.

Note how two of the .. coq:: directives were omitted from the output, and two were kept (can you guess why?). The behavior is basically a compromise between two constraints: the conversion functions should be bijective (modulo whitespace), and their composition should be idempotent. The logic I implemented (though I'm sure I forgot one corner case, or 7), is to remove all .. coq:: markers that can be unambiguously reconstructed from the context. This means removing all markers that (1) do not have custom flags (hence the first preserved header) and (2) have an indentation (nesting) level matching the immediately preceding line (hence the second preserved header, or else when converting back Let aa := 1 would be nested under the .. note::).

Future work

There are a few things that would improve the quality of the documents produced by Alectryon, but I don't have immediate plans to tackle all of them, mostly for lack of time:

Adding a LaTeX backend. This is mostly done.
Working on other advanced visualizations, hopefully culminating in a Coq enhancement proposal to have a standardized way to do non-textual notations (you'd attach a function to a type that says how to render it as a graph, or a LaTeX formula, or an SVG picture, or any other form of rendering). I have early results on this for separation logic; please get in touch if you'd like to hear more.
Extending the system to other languages, probably starting with Lean, F*, easyCrypt, and possibly HOL4? It'd be interesting to see how well this generalizes.
Integrating with jsCoq, to allow users to interact with the code directly in the browser (most of the output would be precomputed, but users would also be able to edit the code and recompute the output). For a mock-up of the experience, see the related tools that I built for F*.
Highlighting differences between consecutive goals, possibly using the support that's now built-in in Coq, though see this issue.
Replacing the coqrst tool used by the Coq refman with a version based on Alectryon, which will likely require merging SerAPI into Coq (pretty please?). (This doesn't mean getting rid of coqdomain.py or changing the syntax used in the manual, just changing the backend that's used to calculate Coq output). Most of the work is done: I built a prototype for SLE2020.

Ideally, we'd take this opportunity to generate not just highlighted snippets but also JSON output, as a giant regression test (we'd check in the generated JSON, so changes would be indicated by git diff and updating the file would just be a matter of committing it).
Porting Coq's box layout algorithm to JavaScript, or just compiling the existing implementation with js_of_ocaml, and using that to reflow code and messages when page dimensions change. I think CSS is close to being able to support this — I know how to do hov boxes (mostly), but I'm not sure whether hv boxes can be done (and in any case, it would likely be quite slow). It's funny that pretty-printing is a whole subfield of PL, but we've never managed to get implementers of web browsers interested.
Integrating Alectryon with CI to automatically produce annotated listings for all files in a repository.

Let me know if you're interested in tackling one of these. I'd love to work together or offer tips / pointers.

Systems and
Formalisms Lab