Zulip Chat Archive

Stream: general

Topic: building doc locally


view this post on Zulip Sorawee Porncharoenwase (Jan 17 2021 at 13:39):

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.

view this post on Zulip Sorawee Porncharoenwase (Jan 17 2021 at 13:57):

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.

view this post on Zulip Rob Lewis (Jan 17 2021 at 13:59):

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

view this post on Zulip Rob Lewis (Jan 17 2021 at 14:00):

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

view this post on Zulip Rob Lewis (Jan 17 2021 at 14:07):

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.

view this post on Zulip Sorawee Porncharoenwase (Jan 17 2021 at 14:56):

Thanks! :)

view this post on Zulip Eric Wieser (Jan 17 2021 at 15:11):

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

view this post on Zulip Rob Lewis (Jan 17 2021 at 15:13):

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!


Last updated: May 14 2021 at 00:42 UTC