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

Rocq 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 VSCode or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Rocq is to manually copy Rocq'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 Rocq'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 Rocq IDE for writing proofs.