Zulip Chat Archive

Stream: general

Topic: mdbook for documentation


Matthew Ballard (Feb 18 2022 at 18:14):

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

Matthew Ballard (Feb 18 2022 at 18:16):

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 (Feb 18 2022 at 18:17):

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

Matthew Ballard (Feb 18 2022 at 18:18):

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

Sebastian Ullrich (Feb 19 2022 at 16:26):

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 (Feb 19 2022 at 16:53):

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

Matthew Ballard (Feb 21 2022 at 16:45):

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 (Feb 24 2022 at 09:21):

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 (Feb 24 2022 at 12:44):

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 (Feb 24 2022 at 13:24):

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 (Sep 06 2022 at 22:06):

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 (Sep 16 2022 at 18:01):

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 (Sep 18 2022 at 12:25):

@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 (Sep 19 2022 at 10:55):

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

Tomas Skrivan (Sep 19 2022 at 10:57):

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

Sebastian Ullrich (Sep 19 2022 at 11:00):

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

Tomas Skrivan (Sep 19 2022 at 11:15):

@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 (Sep 19 2022 at 11:17):

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 (Sep 19 2022 at 11:26):

@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 (Sep 19 2022 at 16:50):

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.


Last updated: Dec 20 2023 at 11:08 UTC