Alectryon, a toolkit for writing technical documents that mix Coq code and prose

Announcements
1

Hi all,

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 .rst to 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!

Happy tangling!
Clément.

12 Likes
2

Awesome @cpitclaudel !

Looking forward to having a jscoq integration as well :grinning:

(I’ve seen you already mentioned it in the blog / section Future work)

3

Congrats on the 1.0 release! Just noting that https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020 will happen soon, in case you’d like to take a slot to present the tool to users.

4

Oh, great idea! But I’m on the job market this year and November 30-december 4th is right around the deadline for faculty applications at many US schools, so I expect I won’t have much time on those days. I’ll send you a PM to see if we can brainstorm something that works.

5

This is very useful!

Do you think it is possible to also make hyperlinks from the terms to their definitions, perhaps by doing a sort of “recursive build”? For example in your blog post you refer to rev_app_distr and it would be really useful to be able to quickly see its definition (in Alectryon-style of course!)

6

Yes, I’m planning on doing this soon. What’s missing at the moment to be able to implement this is described in this SerAPI issue.