Language server starts very slowly.

[wuyoli]

When I started Using this the language server started very slowly (especially when using Mathlib in a project.) It started by compiling all of Mathlib for ~3h on my (relatively slow) Laptop into the .lake folder. Since that is finished It takes "only" ~10min to start while the language server logs stuff like: ⚠ [206/1884] Replayed Mathlib.Logic.ExistsUnique

I set my editor plugin to use the lean binary from the devshell in the flake.Shouldn't this one have access to some kind of prebuilt /Intermediate Binaries? I thought this is what the *.ilean and *.olean` files where for.

[lenianiva]

How are you using the flake? It is normal that the LSP needs to compile the entire mathlib for the first time, but subsequent runs of LSP should be very quick.

A workaround for this could be to not add lean into your shell environment via devShell but rather use elan. This way you only use the Nix packaged Lean during compilation.

[wuyoli]

I use basically the dependency example.

[wuyoli]

I use elan before, but i hoped I could change the workflow to be entirely "nix-based"

[lenianiva]

I use basically the dependency example.

Put pkgs.lean.leanc into the devShell and try that? I think your LSP may be using a mixture of system Lean and Nix based Lean. If this fixes it I'll add it to troubleshooting

[wuyoli]

I would want to have the compiling step when running nix develop instead of when starting the Editor, because this would mean I can let it run on a remote builder (which would be much faster)

Put pkgs.lean.leanc into the devShell and try that?

Tried that, but this doesn't change anything

[wuyoli]

wouldn't it be possible to put the .lake folder in the nix store? this would still not solve the long startup time after the first time.

I still don't understand why it takes so long after that.

[wuyoli]

and yes I confirmed that I'm using the lean binary from the flake