installation doesn't quite work as expected

[holtzermann17]

I refer to the instructions here:

https://github.com/leanprover/mathlib/blob/master/docs/elan.md

These instructions say something a bit confusing, which appears almost contradictory:

1. But if you run leanpkg build from inside my_playground, then it will compile only those files that are dependencies of mathlib group_theory/subgroup.lean.
2. If you want to play more, it's better to compile all your dependencies once and for all. You can do this by going into my_playground and running leanpkg build.

Empirically, if you follow these instructions with an empty ./src directory, nothing happens. I think perhaps the second item should be closer what's said here:

$ cd _target/deps/mathlib/
$ leanpkg build

(That's step 3 from https://github.com/ImperialCollegeLondon/xena-UROP-2018.)

---

Accordingly, I'd suggest the following rewording for that item:

If you want to play more, it's better to compile all your potential dependencies once and for all. You can do this by going into my_playground/_target/deps/mathlib/ and running leanpkg build.

[jcommelin]

Thanks for the suggestion. Voila: #309

[bryangingechen]

I'm surely misunderstanding how this should work, but if I run leanpkg build inside _target/deps/mathlib/ and then run it again in the base directory, lean seems to recompile all the dependencies in mathlib again. I expected lean to realize that the files in mathlib had already been compiled once and that the second build would be much quicker.

Indeed, if I do the slightly perverse thing of alternating leanpkg build in my_playground and my_playground/_target/deps/mathlib/ the builds never seem to stabilize.

I guess my ultimate question is: which build command (or sequence thereof) is optimal for making e.g. vscode as responsive as possible while I edit files importing arbitrary parts of mathlib?

[gebner]

You should only run leanpkg build in my_playground, never in my_playground/_target/deps/mathlib/. (Although I don't really see how that could lead to recompilation.)

[holtzermann17]

@gebner As I noted above, the documentation agrees with what you just said, but I find it confusing. Would it be better to do the following, if the goal is to "compile all your dependencies once and for all"?

$ cd _target/deps/mathlib/
$ lean --make

[jcommelin]

My apologies. I've been messing up. Because #309 just got merged. I would be very grateful if an expert could suggest wording that is not wrong. Because I clearly don't know what I'm doing.

[rwbarton]

What about instead running

$ lean --make _target/deps/mathlib/

from your project directory? I've tried this on a brand-new project and it compiled all of mathlib and things seem to be working as intended, that is, I can now import mathlib files in my project and Lean uses the compiled version, and a subsequent leanpkg build in my project doesn't feel the need to recompile mathlib either. Is this something we could recommend to users?