Global lake environments

Stream: lean4

[Jason Rute]

Right now there is a .lake directory for each project which if Mathlib is installed is 5GB. Many package managers (conda, opam, etc) have both global and local options. So you can either store everything locally like lake does, or have named global enironments like in conda and opam. (I prefer local, but I know others prefer global if just to save space.) Lake doesn't currently have a good way to do global packages, right?

[Jason Rute]

This question came up on https://proofassistants.stackexchange.com/questions/4647/mathlib-is-downloaded-every-time-a-new-project-is-created/4650. The question itself if poorly worded, but in the end this seems to be what they want. They realized you can do packagesDir = "path/to/main/.lake/packages" in the lakefile.toml, but that also means you have to commit a directory path to git, something you don't have to do with other package managers.

[Jason Rute]

You can also use symlinks, but those aren't exactly user-friendly.

[Jason Rute]

I assume the answer is no, but if yes, feel free to post an answer to that question.

[Mac Malone]

Lake support for a system-wide build cache of oleans is on the near-term roadmap (development is currently planned for next quarter). At present, however, packagesDiris the best solution. If I find the time, I could rework it to also support an enviroment vairable (e.g., LAKE_PACKAGES_DIR), which could avoid the need to commit it.

[Eric Wieser]

For what the user is asking there, wouldn't a local mapping that sends "leanprover-community" / "mathlib" to ../some_mathlib_checkout do the trick?

[Eric Wieser]

Which is to say, no olean cache or adjusted build directory is needed, just a way to use existing local dependencies

[Jason Rute]

@Eric Wieser not sure what you mean. Are you saying this is already possible? And if so, how would it work?

[Eric Wieser]

I think there may be a separate feature in the pipeline that does what I describe, which is part of the motivation for the new-style requires in the lakefile. It is "already possible" today by checking out all of the mathlib dependencies, and editing the lakefiles as

 require "leanprover-community" / "batteries" @ git "v4.15.0"
+  from "../batteries"
 require "leanprover-community" / "aesop" @ git "v4.15.0"
+  from "../aesop"

etc

[Jason Rute]

@Eric Wieser Is this much different from the packageDir approach? It still requires putting local file system information in the lakefile. I guess it has the advantage that one doesn’t need a reference .lake directory. (Also if you have no internet connection at all, maybe this would work.)

[Jason Rute]

Also, does one still use lake exe cache get, or will lake build just work?

[Eric Wieser]

If you modify any lakefiles then lake exe cache get will reject any upstream cache

[Eric Wieser]

I believe that the modification I make above also causes lake exe cache pack to fail, as it ignores the lakefile / manifest and hard-codes the location of dependencies. #8767 was an attempt to fix this, but it is frustrating to test

[Mac Malone]

Eric Wieser said:

For what the user is asking there, wouldn't a local mapping that sends "leanprover-community" / "mathlib" to ../some_mathlib_checkout do the trick?

There is the new --packages option which could be used to directly override dependencies, butit requires some more sophiticated know-how and is less than ideal for active development (e.g., it cannot be used with lake update). It is more intended for fixed system configurations (e.g., CIs, testbeds).