Untangling Mechanized Proofs

  • Alectryon does better: it automatically captures Coq'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 Coq IDE for writing proofs.
  • The reason for picking reStructuredText as the markup language for comments is that it's designed with extensibility in mind, which allows me to plug Alectryon into the standard Docutils and Sphinx compilation pipelines for reStructuredText (Sphinx is what the documentations of Haskell, Agda, Coq, and Python are written in).
  • As an example, I made a compatibility shim for Coqdoc that uses Alectryon to render Coq code, responses, and goals, but calls to coqdoc to render the contents of (** … **) comments; look for coqdoc in file cli.py of the distribution to see how it works.

save | report | share on


Top 200 comments