alectryon
Toolkit for literate programming in Coq/Rocq
A library to process Coq and Lean snippets embedded in text documents, showing goals and messages for each input sentence. Also a literate programming toolkit. The goal of Alectryon is to make it easy to write textbooks, blog posts, and other documents that mix interactive proofs and prose. Alectryon originally supported Coq only. Support for Lean is preliminary and restricted to Lean 3.
homepage ↗ github: cpitclaudel/alectryon
Available in
| Overlay | Newest | Ebuilds | Last activity | |
|---|---|---|---|---|
| gentoo gitweb ↗ | 2.0.0 | 1 | 13 h | details › |
Versions & arches
Use flags of 2.0.0
- doc Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
- emacs Add support for GNU Emacs
2 expansion flags (python targets, ABIs, cpu flags…)
- python_targets_python3_13
- python_targets_python3_14
Runtime dependencies of 2.0.0
show 12 lines
python_targets_python3_13?
(
)
python_targets_python3_14?
(
)