CLI tool for generating technical documents with embedded Coq/Lean code
Top 97.2% on sourcepulse
Alectryon is a toolkit for creating technical documents that seamlessly integrate Coq or Lean 4 code with prose. It allows authors to embed code snippets within reStructuredText or Markdown, automatically processing them with Coq/Lean to display interactive proof states, goals, and messages. This is ideal for textbooks, tutorials, and research papers where clear exposition of formal proofs is crucial.
How It Works
Alectryon functions as a library, a Docutils/Sphinx extension, or a standalone compiler. It leverages coq-serapi
to interact with Coq, feeding code snippets and capturing their execution states. For Lean, it integrates with LeanInk. The processed output, including goals and messages, is then embedded back into the source document, typically rendered as interactive HTML. This approach automates the tedious process of manually documenting proof states, ensuring accuracy and interactivity.
Quick Start & Requirements
opam install "coq-serapi>=8.10.0+0.7.0"
python3 -m pip install alectryon
docutils
, sphinx
, myst_parser
, beautifulsoup4
.Highlighted Details
Maintenance & Community
The project is actively maintained by its author, Cyril P. Claudel. Community contributions are welcomed, with examples of use in the wild linked in the README.
Licensing & Compatibility
Alectryon is released under a permissive license, suitable for commercial use and integration into closed-source projects.
Limitations & Caveats
Lean 3 support is preliminary and lacks concurrent processing, literate mode in Emacs, and full quoting capabilities. Some advanced features like marker references and quoting are experimental and subject to syntax changes.
1 day ago
Inactive