I’ve just released Alectryon 1.0!
Alectryon is a collection of tools for writing technical documents that mix Coq code and prose. It includes a compiler that produces interactive webpages from Coq source files, as well as tools to translate back and forth between Coq and reStructuredText, allowing you to toggle between the proof and prose views of a file at will as you edit it. From the blog post:
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.
Alectryon was written with two goals in mind:
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
.rstto see the sources).
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.
As a demo of the latter here’s a full build of Logical Foundations.
Keep reading on the PLV blog for more explanations, demos, and a tutorial, check out the repository to get started using Alectryon, or read the academic paper (open access) for details and plenty of nifty pictures.
Oh, and I have a talk about this at SLE2020 on Monday; you should join!