The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

In the HoTT library, we use proviola to autogenerate documentation that allows playback on hovering (e.g., http://hott.github.io/HoTT/proviola-html/HoTT.Types.Equiv.html , http://hott.github.io/HoTT/proviola-html/toc.html).  We could surely use better css (pull requests welcome!), perhaps even something sphinx-like, but it serves as a nice example because the generation is all done fully automatically on Travis CI.  (The scripts are in etc/ci/*, and if I recall correctly, the relevant one calls `make proviola` in our makefile.)

On Fri, Jun 17, 2016, 5:52 AM Alan Schmitt <alan.schmitt AT polytechnique.org> wrote:

On 2016-06-16 18:30, James Wilcox <wilcoxjay AT gmail.com> writes:

> It's pretty embarrassing to show this dirty hack in public. Surely there is a
> better way!

I don't know if this is better, and it clearly is ugly without a nice
CSS and syntax highlighting (both are easy to set up), but I use
org-mode to document and execute Coq developments. Here is an example
input file http://alan.petitepomme.net/tips/test_coq_exec.org and the
resulting output http://alan.petitepomme.net/tips/test_coq_exec.html.
The glue code to do it is at
http://alan.petitepomme.net/tips/executing_coq.html

To document Coq code from outside the development (if you don't want to
have too much prose in your code), you can use this approach
http://alan.petitepomme.net/tips/documenting_coq.html

Best,

Alan

--
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-05: 403.94, 2016-05: 407.70