Zulip Chat Archive

Stream: Lean for teaching

Topic: Hydras & Co. and snippets for documentation

Karl Palmskog (Dec 19 2021 at 12:22):

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 (Dec 19 2021 at 17:00):

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.

Last updated: Dec 20 2023 at 11:08 UTC