README: clarify line about .olean files

[waldyrious]

Just a small tweak to make the line less cryptic for beginners.

Although, to be honest I still don't fully understand what this sentence is saying — how does one make sure the .olean files are generated in the _target folder, and what exactly will be extremely slow otherwise?

[bryangingechen]

I usually run leanproject up to update the project to depend on the latest mathlib master, or simply leanproject get-mathlib-cache if I don't care what version of mathlib I'm generating the docs for.

See https://leanprover-community.github.io/leanproject.html#getting-mathlib-oleans

[bryangingechen]

We most likely don't want to link to that tutorial which is very out of date. It's better to link to the community webpage on leanproject.

[waldyrious]

Sure, I can remove the link — just changing from "olean files" to ".olean files" already helps making things a little clearer, IMO. I could replace the link with https://leanprover-community.github.io/leanproject.html instead, but I don't think that page (in its current state) provides the information one would expect when clicking on the expression ".olean files" (i.e. additional details on what .olean files are).

That said, depending on the outcome of the conversation at leanprover-community/leanprover-community.github.io#180, it could make sense to add the link here. I'd suggest holding this PR until that one is resolved, so we can decide what makes the most sense here.

[bryangingechen]

what exactly will be extremely slow otherwise?

If the .olean files are not present, generating the docs will take a long time since Lean will have to compile all of mathlib from scratch.

[jcommelin]

Which easily takes 2 hours.