## Stream: general

### 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.

Thanks! :)

#### 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

#### 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