mdbook setup template for Lean project

Stream: general

[Asei Inoue]

mdbook is useful for documentation. mdbook will still be a popular tool in Lean project until verso becomes more popular.

I have customised the mdbook for Lean for myself. It supports Lean syntax highlight and MathJax, as well as the ability to jump to the Lean Playground. Various other functions are also supported.

Source of my template is available here. I would be happy if it is useful to someone.
https://github.com/Seasawher/lean-book

[Florent Schaffhauser]

The links in /md/SUMMARY.md seem incorrect?

And when I follow the instructions in /Src/HowToUse.lean and run lake build and mdbook serve --open, I get the following error:

2024-03-20 21:35:46 [ERROR] (mdbook::utils): Error: Chapter file not found, ./README.md
2024-03-20 21:35:46 [ERROR] (mdbook::utils):    Caused By: No such file or directory (os error 2)

I did modify the links by hand to check what happens, but then I still don't get the same rendering as in the template. The highlighting, in particular, is not working for me :thinking:

[Florent Schaffhauser]

OK, sorry, I understood my mistake. And I managed to fix it by running successively:

lake exe mdgen "Src" "md"
lake exe import_all "Src"
mdbook build
mdbook serve --open

But somehow, if I try lake run build instead, I get the message:

could not execute external process 'lake exe mdgen'

[Asei Inoue]

I don’t know why “external process” error occurs. But I have seen the same error when running ‘lake run build’ in GitHub action. What’s your OS?

[Florent Schaffhauser]

macOS

[Asei Inoue]

"could not execute external process" error may mean that elan in your environment is broken. Why don't you elan self update, delete the .lake directory and try again?

[Florent Schaffhauser]

Thanks for looking into this! I tried what you suggested and I now have elan 3.1.1 but, even after removing the .lake directory, the problem persists :oh_no:

[Florent Schaffhauser]

However, if nobody else reports a similar issue, it may indeed be a problem with my installation, I just don't know what it is. In any case, I can still generate the html files from the template, I just have to input lake exe mdgen "Src" "md" manually.

[Florent Schaffhauser]

Hi :smile:

Here is the same error that I get on my machine but reproduced on Codespaces and directly from the lean-book repo after installing elan and lean:

Image-22-03-2024-at-15.04.jpeg

If I try to comment out the first line of the script in lakefile.lean

def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
  let out ← IO.Process.output {
    cmd := cmd
    args := args
  }
  let hasError := out.exitCode != 0
  if hasError then
    IO.eprint out.stderr
  return hasError

script build do
--  if ← runCmd "lake exe mdgen" #["Src", "md"] then return 1  -- I commented this line out
  if ← runCmd "lake exe import_all" #["Src"] then return 1
  if ← runCmd "mdbook build" #[] then return 1
  return 0

then the error becomes

could not execute external process 'lake exe import_all'

so maybe the problem is related to the way the script is interpreted by the machine?

[Sebastian Ullrich]

@Asei Inoue Are you on Windows? Putting arguments like exe in cmd is definitely wrong on Unix platforms

[Florent Schaffhauser]

Oooh, I see the issue now :face_palm: Here's a fix that works for me then:

script build do
  if ← runCmd "lake" #["exe", "mdgen", "Src", "md"] then return 1
  if ← runCmd "lake" #["exe", "import_all", "Src"] then return 1
  if ← runCmd "mdbook" #["build"] then return 1
  return 0

[Asei Inoue]

@Sebastian Ullrich Yes, I use Windows.

[Asei Inoue]

@Flo (Florent Schaffhauser) Thank you very much!

I had not noticed this mistake for a long time ... Thanks for correcting it.

I made the same mistake in the metaprogramming book. I have corrected it.