How long does it take to initially build a mathlib proj?

Stream: new members

[Daniel Donnelly]

The infoview in vscode just keeps saying "✔ [240/862] Built Mathlib.Tactic.Attr.Core", and the number is changing but then it goes back down, then up, then down, etc.

So, I'm wondering how long this will take, and if users want to distribute their project, I'm assuming they can pre-build to .olean files? Is that correct - and that would speed up this stage of the process?

In other words, Lean or Lake seem to be spinning on something, and so I can't begin type-checking yet.

[Michael Rothgang]

Are you working on mathlib itself or on a project depending on mathlib?

[Daniel Donnelly]

@Michael Rothgang thank you 🙏🏾 It's a mathlib-based project, because I need all these number theory definitions.

[Michael Rothgang]

Usually, you should not need to build these low-level files yourself: "get the cache" instead, and download pre-built oleans. On the terminal, you can use lake exe cache get. (Make sure to close any open files in VS Code that are building mathlib in parallel. If you want to be really sure, close VS Code and kill any running lean processes.)

[Michael Rothgang]

In VS Code, click on the \forall icon and choose Project Actions -> Fetch Mathlib Build Cache do so so.

[Daniel Donnelly]

So I can run that from any terminal/ current directory in windows?

[Notification Bot]

This topic was moved here from #mathlib4 > How long does it take to initially build a mathlib proj? by Michael Rothgang.

[Michael Rothgang]

(Let me move this to a different stream, where you are more likely to be helped.)

[Michael Rothgang]

Daniel Donnelly said:

So I can run that from any terminal/ current directory in windows?

Yes, you can either do this clicking in VS Code, or you can run lake exe cache get from the terminal in your project's root directory. Both will do the same thing (so you only need to do one of them :-))

[Daniel Donnelly]

Cool :sunglasses: it's running: lake exe cache get

[Daniel Donnelly]

I'm formalizing a new result in NT

[Daniel Donnelly]

Mostly in order to learn Lean4 itself, though

[Daniel Donnelly]

Michael Rothgang said:

(Let me move this to a different stream, where you are more likely to be helped.)

Thanks @Michael Rothgang for your responsiveness. You greatly helped. Lean4 is type checking, "intellisense" is working, etc.