building doc locally

Stream: general

[Sorawee Porncharoenwase]

I follow the instructions at https://github.com/leanprover-community/doc-gen to build the doc locally. The lean src/entrypoint.lean step takes forever for me (it's been 20 mins, and still has not finished). The README does talk about how I should "Make sure that olean files are generated". Otherwise, it will be "extremely slow." But I do have .olean files (queried via find . -name '*.olean'). Do you know what could go wrong?

Looking at the CI, I found that gen-docs (which calls lean src/entrypoint.lean) should take only 15 mins.

I'm on Macbook M1, FWIW.

[Sorawee Porncharoenwase]

OK, it finally terminates, after running for 30 mins.

Any pointer for how to speed this thing up would be greatly appreciated, but it's good news that it does terminate after all.

[Rob Lewis]

You can make sure the oleans are up to date by running leanpkg configure and then leanproject get-mathlib-cache. But 30 min sounds fast for a full mathlib + docs build so this might not be the problem

[Rob Lewis]

doc-gen isn't fast but 30 min does sound kind of slow

[Rob Lewis]

I should also warn you, the default mathlib version for doc-gen is some random old commit. The CI script has a step that updates it to the latest mathlib. You should run leanproject up if you want docs for current mathlib.

[Sorawee Porncharoenwase]

Thanks! :)

[Eric Wieser]

Are you building it to preview new markdown you're writing, or because you want to adjust the build process itself? In both cases, I think there are ways to avoid having to re-run entrypoint.lean

[Rob Lewis]

Rob Lewis said:

doc-gen isn't fast but 30 min does sound kind of slow

FWIW it runs in 4:30 on my laptop. So I guess you had old oleans and the M1 is fast enough to build mathlib in 30 min!