Is it normal to have to compile thousands of modules (?)

Stream: mathlib4

[Spearman]

I tried adding mathlib4 to my project so I could use the #help syntax. When running it, it gets stuck building what looks like a large number of object files:

⣻ [6019/10030] Running Mathlib.Tactic.CC.Addition:c.o (+ 7 more)

At the current rates it's going to take about an hour, but I also have to stop it occasionally because it is using 100% CPU and overheating my computer. Also my project directory is now taking up 4.5GB.

[Ruben Van de Velde]

No, that's what lake exe cache get is for

[Yury G. Kudryashov]

What do you import?

[Spearman]

I've already run lake exe cache get, it says it completed successfully. As soon as I import Mathlib in my .lean executable and do lake exe myproject it starts building again from [5010/10034].

[Yury G. Kudryashov]

You should import a specific file instead.

[Spearman]

Which file should I import to access #help?

[Yury G. Kudryashov]

While cache gives you oleans, executables need to compile files (i.e., build .o files).

[Yury G. Kudryashov]

Mathlib.Tactic.HelpCmd

[Yury G. Kudryashov]

Do you need it at runtime, or only during development?

[Yury G. Kudryashov]

Never mind, it has very few dependencies.

[Patrick Massot]

That 10.000 is very suspicious, it looks like you depend you two copies of Mathlib (which is 5000 files long). Could you share your lakefile.lean (or lakefile.toml)?

[Sebastian Ullrich]

It's probably olean+o, the first half of which cache has already handled

[Mario Carneiro]

building .o files should not take an hour

[Mario Carneiro]

a long time ago it was 5 minutes, so maybe it's 15 minutes now?

[Mario Carneiro]

The most straightforward way to not have to build .o files for a lot of mathlib is to not import that much - avoid import Mathlib, and instead import only the files you actually need for execution in your lean_exe target. You can have another lean_lib with proofs about your program if you need more of mathlib for that

[Mario Carneiro]

Generally speaking, you shouldn't need much if anything of mathlib in an executable. Most of the things that you might need are candidates for moving to batteries if they aren't already in it or in core

[Jon Eugster]

Just to reiterate what Mario says, in most cases when people create a new Lean project and then add Mathlib, they actually want to delete the file Main.lean from the newly created Lean project and delete the part which says lean_exe from the lakefile. (depending on which arguments you used in lake new it may or may not have created such a stub executable for you)

If you want to write mathematical proofs, you don't need Main.lean or the executable. You only need it if you want to write an executable like lake exe my-program