Closed holtzermann17 closed 5 years ago
Thanks for the suggestion. Voila: https://github.com/leanprover/mathlib/pull/309
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?
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.)
@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
My apologies. I've been messing up. Because https://github.com/leanprover/mathlib/pull/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.
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?
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:
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:(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.