mdbook for documentation

Stream: general

[Matthew Ballard]

I noticed with Lean 4 there has been a migration to mdbook for narrative-style documentation: the Lean 4 manual and TPIL4.

[Matthew Ballard]

I :heart: mdbook as I envision a workflow where my papers/course notes/etc... start as mdbook documents and get processed into tex or something else. Plus it is easy to set up, work with, and modify.

[Matthew Ballard]

I was wondering: is this part of some broader plan for this type of documentation for Lean?

[Matthew Ballard]

(Note: this is separate from API documentation which also is wonderful)

[Sebastian Ullrich]

I wouldn't say there's a grand plan behind it. We chose mdbook because it looks good, and because everyone knows Markdown.

[Matthew Ballard]

I was secretly hoping there was a formally specified enhanced markdown language with parser implemented in Lean 4 coming. :joy:

[Matthew Ballard]

More seriously, one feature mdbook has that I haven't seen in other generators is the ability to pipe the markdown out to an existing binary and then pipe it back in via stdout/stdin. This way you can use preprocessors that written in anything.

[Eric Wieser]

Other tools like Sphinx take the approach of letting you declare new syntax blocks, and handle them in-process where you have access to the parses state of the document. Preprocessing markdown via the standard streams sounds fragile, especially if your binary expects a different dialect of markdown to what mdbook uses.

[Matthew Ballard]

Oh, I should have been more clear. Mdbook has easily extensible syntax in the usual way for generators. Piping everything in and out would be an eccentric choice.

I highlighted that ability to emphasize the commitment to flexibility. Since getting tired of Jekyll build times I’ve tried to find a speedier option that allowed the same level of extensibility. Hugo is fast and has a vast ecosystem but it’s not very flexible. I haven’t used Sphinx but I assume it’s build times are comparable to Jekyll?

[Eric Wieser]

My experience of sphinx is usually that it's slow, but that's because the extensions I run it with end up executing arbitrarily slow python code of my own... Conversely, I've never used mdbook!

[Dan Velleman]

I'm interested in writing a document that will include Lean examples, including examples of errors. I'd like the examples of errors to show the red wavy lines that Lean uses to indicate errors. Can that be done in mdbook? Would it require changes in highlight.js?

I have never used mdbook or any similar system--Sphinx, Quarto, etc. I don't know python. So I'm looking for the system that would easiest for a beginner to use.

[Chris Lovett]

Yeah, I was recently writing the chapter on monads for lean 4 using mdbook with a preprocessing toolchain based on https://github.com/leanprover/LeanInk/ and https://github.com/Kha/alectryon, and I too ran into the need to show some red squiggles on this code snippet, so I opened this issue: https://github.com/leanprover/LeanInk/issues/34. The fix would be for leanink to convey the information in the json file so that alectryon can put the red squiggles in the right place. Should not be too hard to do. The LeanInk toolchain for example, does format the lean snippet with a tooltip that shows the error when you hover in the right place which is cool - we just need the red squiggle to show the user they can hover in that location.

image.png

[Tomas Skrivan]

@Chris Lovett I was looking at your chapter on monads and wanted to replicated your workflow but I failed. How do you turn literate *.lean file into *.md file? I have managed to get only html or rst file.

[Arthur Paulino]

@Tomas Skrivan this might do if you're stuck:
https://github.com/arthurpaulino/lean2md

[Tomas Skrivan]

Cool, is it using LeanInk/Alectryon? I want the expandable states. Also does it support Lean 4?

[Sebastian Ullrich]

@Tomas Skrivan Have you seen https://leanprover.github.io/lean4/doc/dev/mdbook.html#build?

[Tomas Skrivan]

@Sebastian Ullrich I think the mistake I was doing is that I didn't use your fork of Alectryon. The command alectryon --frontend lean4+markup examples\palindromes.lean --backend webpage -o palindromes.lean.md didn't work for me with the vanilla version.

[Sebastian Ullrich]

Yeah, the fork situation is not ideal. It doesn't help that we don't know in which direction we should continue, sticking with Alectryon or moving towards doc-gen4.

[Arthur Paulino]

@Tomas Skrivan it's a purely syntactical converter. It works for Lean 3 and Lean 4 (that's what we used to create the markdown files for the metaprogramming book)

[Chris Lovett]

Hi Tomas, I have a build script like this:

@echo off
for %%i in (*.lean) do (
   if not "%%i" == "lakefile.lean" (
      echo ==================== %%i
      echo alectryon --frontend lean4+markup %%i --backend webpage --lake lakefile.lean -o %%i.md
      alectryon.exe --frontend lean4+markup %%i --backend webpage --lake lakefile.lean -o %%i.md
   )
)

mdbook build
start out\index.html

note the --lake lakefile.lean is only needed if your lean files have dependencies described in a lakefile. The reference manual does not have this, but other projects might, especially if you want one .lean file to be able to import another to bring dependencies across chapters.