Caching .lake

Stream: lean4

[Leni Aniva]

If I have a pre-built version of one of the dependencies in lake-manifest.lean, is there any way to inject that into Lean LSP's running environment?

The use case is this: If I can pre-build a giant dependency like Mathlib, any user of my library can simply fetch that dependency and store it in somewhere convenient like /nix, and doesn't have to take 3 hours for their LSP to fire up for the first time.

I think this will involve suppressing the Replay function in src/lake/Lake/build/Job.lean

[Johan Commelin]

This is certainly possible, because we do that with mathlib using lake exe cache get. You will have to distribute the olean files of your pre-built version.

[Leni Aniva]

Johan Commelin said:

This is certainly possible, because we do that with mathlib using lake exe cache get. You will have to distribute the olean files of your pre-built version.

Are both .olean and .ilean files required?

From what I read in the lake README.md, it seems like I need to add the .olean/.ilean tree to LEAN_PATH and the Lean src tree to LEAN_SRC_PATH

[Damiano Testa]

I do not know whether both oleans and ileans are needed, but the former contain most of the Expr information, while the latter contain "hover" information (and should be much smaller in size). Even if you could get away with just the oleans, I suspect that you would have a much better experience having both.

[Eric Wieser]

You need absolutely everything in .lake/build, otherwise lake build will say "oh, my .trace/.hash/.c/... files are missing, better rebuild the universe"

[Leni Aniva]

Eric Wieser said:

You need absolutely everything in .lake/build, otherwise lake build will say "oh, my .trace/.hash/.c/... files are missing, better rebuild the universe"

so if I have a pre-built version of .lake/build, I should put it in LEAN_PATH?

[Leni Aniva]

In Lake's documentation, it says

This search path can be augmented by including other directories of Lean libraries in the LEAN_PATH environment variable (and their sources in LEAN_SRC_PATH).

but it doesn't say what needs to go into LEAN_PATH and LEAN_SRC_PATH.