alectryon  by cpitclaudel

CLI tool for generating technical documents with embedded Coq/Lean code

created 5 years ago
265 stars

Top 97.2% on sourcepulse

GitHubView on GitHub
Project Summary

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

  • Install via OPAM: opam install "coq-serapi>=8.10.0+0.7.0"
  • Install via pip: python3 -m pip install alectryon
  • Requires Coq $\ge$ 8.10 (8.12+ recommended). Lean 4 support requires LeanInk.
  • Optional dependencies for specific backends: docutils, sphinx, myst_parser, beautifulsoup4.
  • Official quick-start guide: https://systemf.epfl.ch/blog/alectryon/

Highlighted Details

  • Supports Coq and Lean 3/4.
  • Integrates with Sphinx and Docutils for documentation generation.
  • Advanced features include marker-based selection of proof states, output assertions, and linking to Coq identifiers.
  • Caching mechanism speeds up recompilation and allows deployment without a full Coq environment.

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.

Health Check
Last commit

1 day ago

Responsiveness

Inactive

Pull Requests (30d)
1
Issues (30d)
0
Star History
11 stars in the last 90 days

Explore Similar Projects

Feedback? Help us improve.