lean documentation

Stream: new members

[Yufei Liu]

Is there anyway to nicely align lean code with comments? such as a lean markdown? or a overleaf package with lean plug-in that kind of thing?

[Utensil Song]

There are at least 3 things related to your question:

1. doc-gen4 generates doc for Lean projects, Mathlib4 uses it, it supports markdown with math. But it's "API document" style, that means you can't write -- style comments inside a proof or a function and expect it renders markdown. You need to write Lean code block in Markdown like you write code in other languages in Markdown, so the Lean code block you are explaining step by step is not executable, thus less maintainable.

This is the easiest way to get Lean work with Markdown, and has official and wide usage.

2. alectryon supports literate programming for Coq and Lean in both direction: Lean in markup + markup in Lean, and the Lean is still executable in both cases. The downside is that it officially supports only reStructuredText, to use Markdown, you need to use this fork Kha/alectryon@typeid and follow how Lean 4 Manual uses it. I don't know if anyone has a simpler workflow for this, I have a simple setup here inside annotate_all.sh. And a simple example is here. Note that this way Markdown is pass-through, and you need to render Markdown yourself, like I have chosen markdown-it-py to do it.

The major advantage of this method is that the reader can inspect types, tactic states and outputs by #eval, #check etc.

It has the same issue that you can't comfortably mix Lean with Markdown. It supports only /-! style doc, and even if I hacked it to support /-- style, the render result messed with the indentation because alectryon breaks a code block into code blocks and comment blocks, so indentations are eaten.

A liter solution is to render annotations from LeanInk, which is JSON.

This way is semi-official because Lean 4 Manual uses it, but it's not easy to use thus not widely adopted.

3. Listing Lean code in LaTeX like on overleaf is officially supported and used by many papers (not sure if they are using the same method or each has some improvements, but this is the baseline solution): https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html

Other methods are mostly manual, you need to manually maintain the correctness of the Lean code and the tactic states, like in many online books about Lean.

[Mario Carneiro]

A variation on 2 which is worth mentioning is the framework developed by David Thrane Christiansen for FPIL: https://github.com/leanprover/fp-lean . I believe it is similar to the Lean 4 book but it has more features to check the correctness of code blocks against claimed outputs

[Yufei Liu]

thank you guys for such detailed reply, i'll check them out!

[Utensil Song]

I've checked the features in https://github.com/leanprover/fp-lean , but it requires writing the Lean proof in a style that's friendly to regex match but human readers, and deviates from normal Lean proof, thus less desirable.

There's also a pain point that wrapping normal proofs in macros make it less "clickable" in VS Code. It's easy to click into the macro instead of the tactics, theorems etc.