Topic: building doc locally
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.
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.
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
Rob Lewis (Jan 17 2021 at 14:00):
doc-gen isn't fast but 30 min does sound kind of slow
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.
Sorawee Porncharoenwase (Jan 17 2021 at 14:56):
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
Rob Lewis (Jan 17 2021 at 15:13):
Rob Lewis said:
doc-genisn'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