Hydras & Co. and snippets for documentation

Stream: Lean for teaching

[Karl Palmskog]

The camera-ready version of our paper on the "Hydras & Co." project , accepted at JFLA 2022, is now available: https://hal.inria.fr/hal-03404668

The project consists of a Coq repository formalizing the theory of ordinals and other discrete mathematics, and a continuously updated PDF book that describes both the math and the code.

For the Lean community, we believe our toolchain that allows snippets from "live" proof assistant code to be executed and be pretty printed with its output using Alectryon could be of interest to authors of textbooks. As you may know, Lean already has experimental Alectryon support, and our tooling could be adapted on top of that.

See here (Figure 8 in the paper) for a nice example of what snippet-based documentation can look like.

With P. Castéran, J. Damour, C. Pit-Claudel and T. Zimmermann.

[Karl Palmskog]

Note also that our toolchain was recently used by someone other than the authors to produce slides with Beamer based on code from a "live" Coq development. The corresponding discussion in Coq's Zulip is here.