Coq meets literate programming: tools for documenting, preserving, and sharing
summary
Alectryon is a literate‑programming toolkit that records Coq output and embeds captured goals and messages into pre‑rendered HTML so proofs are instantly explorable without running Coq; it also generates HTML and reStructuredText (and can produce LaTeX/PDF), supports EasyCrypt/Lean work in progress, and can replace a simple coqc command in build scripts. It provides post‑processors to render graphs or assembly, caches outputs for reproducible archives and flags changed outputs; the core pipeline works today though rich visual layouts (continuous, stable graph placement) remain hacky and need further engineering.
AI-written summary · about
chapters (12)
- 0:00Start
- 5:23Math Proofs
- 10:43Correctness for a Compiler
- 17:02Construct a Proof
- 24:30Post Processing
- 27:35Demo
- 32:15Annotations
- 40:43External Documentation
- 42:07Per-Object Documentation
- 44:17The Separation Logic Formula
- 50:29Alternative Notation Domains
- 53:02Multiple Domains
related talks
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions
31mLiterate Tracing
19mTowards Mining Robust Coq Proof Patterns
19mReproducible, dynamic, and elegant books with Quarto
10mShow, Don't Tell
27mProduction Language Specification - Requirements for Multiple Usages
50mContinuous and Automated Documentation Docs As Code in Practice
47mDocumentation as code (explained to my dad)