Literate Lean

Stream: Lean for teaching

[Philip Wadler]

Apologies if this is a newbie question, but I am a Lean newbie.

I've written an online textbook, Programming Language Foundation in Agda (plfa.inf.ed.ac.uk), and am considering adapting it to Lean. In the textbook, each chapter is a separate markdown file containing literate Agda. The beginning of the chapter needs to import relevant bits of the standard library, but then everything subsequent in the chapter can make use of any definitions, lemmas, and so on from earlier in the chapter. Let's call this "literate" style. (It descends from Donald Knuth's Literate Programming, via the literate style for Haskell introduced by Richard Bird.)

In contrast, in Theorem Proving in Lean (https://leanprover.github.io/theorem_proving_in_lean/), each code snippet is independent. Every example needs to import anything relevant from mathlib or from earlier in the chapter. There is support for hiding lines that import from mathlib or copy earlier developments in order to make the text more readable. Let's call this "snippet" style.

My question is, do there exist tools for Lean that support the "literate" style as opposed to the "snippet" style? I couldn't find any with an hour or so of search. Thank you for your help!

[Henrik Böving]

This is not available in Lean 3 right now but in Lean 4 we have LeanInk (https://github.com/leanprover/LeanInk/) which is a lean frontend to the well known coq alectryon (https://github.com/cpitclaudel/alectryon) and is as of this week integrate into the lean 4 docuemtnation tool doc-gen4 (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Defs.html, you can click on the ink button in any Mathlib submodule to see the doc-gen rendered version of the LeanInk output). This isn't nearly as advanced as the alectryon renderer right now but I do plan to push it to the point where we can basically write our books/tutorials whatever with it in this interactive style you are searching for, though this will definitely take some time.

[Arthur Paulino]

This should be compatible with Lean 3:
https://github.com/arthurpaulino/lean2md
Edit: nvm, you need to go the other way around (md to lean, not lean to md)

[Patrick Massot]

The setup in Mathematics in Lean is closer to what you want. See https://github.com/avigad/mathematics_in_lean_source. The actual source is a bunch of Lean files containing restructured text markup, for instance https://github.com/avigad/mathematics_in_lean_source/blob/master/lean_source/07_Topology/source_01_Filters.lean. The point of using a Lean file is that you can get feedback from Lean while writing. It could be adapted easily to use md instead of rst (Jeremy was used to restructured text instead of markdown).

[Patrick Massot]

However this is still a hack. We are refraining to seriously work on such tools until we really switch to Lean 4.

[Jeremy Avigad]

Jeremy was used to restructured text instead of markdown

I am actually o.k. with both. Restructured text has some advantages over markdown, like better mechanisms for including links, references, figures, and math formulas. (Google will provide various comparisons.)

The Python scripts used to generated the files for MIL are pretty rudimentary. I wrote them in a rush, so there is definitely room for improvement. But they work really well, and it is extremely helpful to write the text and the Lean in the same file. For years I would write the text in one file and the Lean examples in another and then cut and paste. This is much better. It also made it easier to generate files containing solutions to the exercises -- i.e. you write the exercise and the solutions in the same Lean file, and some simple markup indicates which is which.

We have also talked about connecting this with Alectryon / Lean Ink so that readers can step through proofs by hovering over the text in the browser.

[Eric Wieser]

Another advantage of restructured text is that it has extensibility built in in a standardized way (custom :role:s and .. admonition::s). As far as I can tell, the main downside is that in practice it's more of a standard implementation than a specification, which means we have to have python in the system somewhere and can't really put the whole thing in lean itself.

[Henrik Böving]

After my exams in july i was planning on porting the CMark renderer we use for markdown in doc-gen right now to pure Lean so we can also reuse it nicely in the LeanInk rendering. Is there a clear preference here? I'll be happy to implement either of them but not both at the same time, at least not while the rest isn't fleshed out.

[Eric Wieser]

CMark is what doc-gen4 uses? doc-gen3 uses mistletoe, but I was planning to port it to markdown-it once an upstream math-formatting patch is merged

[Eric Wieser]

(I think markdown-it is what vscode uses internally)

[Henrik Böving]

Yeah we use cmark to avoid any other language dependencies, CMark is a C lib and since you already necessarily have a c compiler when you compile Lean 4 that's just natural, the move away from mistletoe was intentional.

[Eric Wieser]

CMark doesn't support math, right? (edit: https://github.com/commonmark/cmark/issues/439)

[Henrik Böving]

Not to my knowledge no, but that (among getting rid of the dpendency on pure C as well :D) is one of the reasons I want to look into writing a renderer in pure Lean 4. So naturally the question comes up whether it should be a markdown or RST one. But given that we probably want to render math it looks like RST is going to win huh?

[Eric Wieser]

In principle you could probably compile markdown-it (javascript) to a C interface via Emscripten, then call that from Lean?

[Henrik Böving]

I guess that might be possible yeah, though I dont really see the advantage over CMark at that point?

[Eric Wieser]

The fact that you get math support (via an extension), without having to write everything from scratch

[Chris Lovett]

Getting back to Phillips original question, yes it is possible now that we have LeanInk and alectryon and mdbook working together :-) I believe the following example is following the Literate Style of writing a book. This Natural Numbers Tutorial (derived from the famous Natural Number Game) is written in Lean then uses LeanInk to create markdown then it uses mdbook to generate nice HTML with a TOC on the left, the TOC comes from SUMMARY.md. The result looks like this https://lovettsoftware.com/NaturalNumbers/. Each code block in each .lean file can build on previous code blocks and each file can also import previous sections to build on those and so on. Notice the mdbook is enabling mathjax so you can even do inline latex formulas if you want like you see in Function World Level5 with the expressions \\(10^{10^{10}}\\) which is rendered like this:
image.png

[Alex J. Best]

Really nice!
I noticed the github links in the top right go to the wrong url though: https://github.com/leanprover/lean4-samples/NaturalNumbers rather than https://github.com/leanprover/lean4-samples/tree/main/NaturalNumbers

[Heather Macbeth]

@Chris Lovett Nice work! For my own applications (typical example: html and the code it's built on 1 2) I would like to show only snippets of the full source code, with other parts hidden. For example, no need to show the reader this:

/-
Copyright (c) 2022 Heather Macbeth. All rights reserved.
Authors: Heather Macbeth
-/
import data.mv_polynomial.pderiv
import data.mv_polynomial.comm_ring
import tactic.polyrith
import tactic.norm_fin

noncomputable theory

open mv_polynomial

variables (K : Type*) [field K] [char_zero K]

/-! This file contains a lot of computationally-intensive evaluation of polynomials and their
derivatives. We speed it up slightly by specifiying in advance the path the simplifier should take.
-/

mk_simp_attribute poly_simps "simp-lemmas for polynomials"

attribute [poly_simps] mv_polynomial.eval_X mv_polynomial.eval_C
  map_add map_sub map_mul map_neg map_bit0 map_bit1 map_one map_pow map_zero
  matrix.cons_val_zero matrix.cons_val_one matrix.head_cons
  matrix.cons_vec_bit0_eq_alt0 matrix.cons_vec_bit1_eq_alt1
  matrix.cons_vec_alt0 matrix.cons_vec_alt1
  matrix.cons_append matrix.empty_append
  derivation.leibniz derivation.leibniz_pow pderiv_C pderiv_X_of_ne pderiv_X_self pi.single_eq_of_ne
  algebra.id.smul_eq_mul nsmul_eq_mul
  nat.cast_bit1 nat.cast_bit0 nat.cast_one
  -- `ring`/`linear_combination` would take care of the next ones, but we add them to aid human
  -- inspection
  mul_zero zero_mul mul_one one_mul add_zero zero_add pow_one mul_neg neg_zero

[Heather Macbeth]

Is this possible?