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

[lenianiva]

I'll ask on Lean zulip to see if we can cache .lake. https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Caching.20.2Elake/near/482539207

I'll look into why this happens and if it is possible to cache the dependency build files, but please keep in mind what we provide here is just a way to build the Lean executable. Everything after that executable is shipped is outside of our control (e.g. suppressing the Replay behaviour from lake). I'm happy to provide dependency caching if it can be implemented in Nix (I certainly hope so), but I can't promise it.

[lenianiva]

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.

I don't know if the LSP Lean will let you do that. I asked on the Lean zulip chat. For the replay, are you sure this behaviour doesn't happen with elan lean?

[lenianiva]

Can you try #26 and add pkgs.lean.lake into the devShell and see if it works?

This would replace the system lake as well.

[wuyoli]

I don't have a system-wide Installation of lake, lean or elan installation. All i ever had was a previous devShell with the elan package from nixpkgs.

[lenianiva]

I don't have a system-wide Installation of lake, lean or elan installation. All i ever had was a previous devShell with the elan package from nixpkgs.

What if you clean the .lake directory and re-run lake build with the flake lake? This should build the dependency cache and you'll be able to launch LSP afterwards. It will take a while though.

[lenianiva]

If that still doesn't work, I have a solution that can make this true:

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.

but I first have to confirm it with the folks on Lean zulip.

[wuyoli]

when I changed to the lean4-nix flake I accidentally did two things:

• I downgraded the lean-toolchain file from leanprover/lean4:v4.13.0-rc3 because of some Errors which I got without doing that
• I updated the nixpkgs input of my flake. In his updated version the elan package does for some reason not provide the elan binary (but the lake and lean binaries).
  the lean version change seems to have broken some stuff. I'm now trying if switching back makes it faster again, but it is compiling again.

[lenianiva]

when I changed to the lean4-nix flake I accidentally did two things:

* I downgraded the `lean-toolchain` file from `leanprover/lean4:v4.13.0-rc3` because of some Errors which I got without doing that

* I updated the nixpkgs input of my flake. In his updated version the `elan` package does for some reason not provide the `elan` binary (but the `lake` and `lean` binaries).
  the lean version change seems to have broken some stuff. I'm now trying if switching back makes it faster again, but it is compiling again.

Please don't use any of the release candidates. If you look at the manifests/ directory there's only support for the major versions v4.{11,12,13}.0. The release candidate will not have support and things may randomly fail.

elan is not provided since elan manages the lake and lean versions. Since we provide version management via nix we don't need elan.

[wuyoli]

Please don't use any of the release candidates. If you look at the manifests/ directory there's only support for the major versions v4.{11,12,13}.0. The release candidate will not have support and things may randomly fail.

yes, I read that and that is why i tried downgrading the version. I used this in the first place because Mathlib officially recommends to use the rc-versions of lean

elan is not provided since elan
manages the lake and lean versions. Since we provide version management via nix we don't need elan.

then why Is there a Package called elan?

[wuyoli]

I'm now trying if switching back makes it faster again, but it is compiling again.

This didn't help it's still replaying stuff

[lenianiva]

Please don't use any of the release candidates. If you look at the manifests/ directory there's only support for the major versions v4.{11,12,13}.0. The release candidate will not have support and things may randomly fail.

yes, I read that and that is why i tried downgrading the version. I used this in the first place because Mathlib officially recommends to use the rc-versions of lean

Why don't use use the v4.13.0 tag for Mathlib? That documentation you linked doesn't say anything about the release candidates.

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.13.0"

elan is not provided since elan
manages the lake and lean versions. Since we provide version management via nix we don't need elan.

then why Is there a Package called elan?

Not in this flake.

[lenianiva]

I'm now trying if switching back makes it faster again, but it is compiling again.

This didn't help it's still replaying stuff

Can you ask on Lean 4 zulip about what could cause lake to replay all dependencies?

[wuyoli]

Can you ask on Lean 4 zulip about what could cause lake to replay all dependencies?

I'm pretty sure lake behaves differently with self-built binaries vs binaries from the cache.

then why Is there a Package called elan?
Not in this flake.

But in nixpkgs.

That documentation you linked doesn't say anything about the release candidates.

it tells me to run:

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

this link currently contains leanprover/lean4:v4.14.0-rc2 and contained leanprover/lean4:v4.13.0-rc3 a while ago when I started using Mathlib.

[lenianiva]

Can you ask on Lean 4 zulip about what could cause lake to replay all dependencies?

I'm pretty sure lake behaves differently with self-built binaries vs binaries from the cache.

That is not very specific. Could you pin down what behaviour is different?

then why Is there a Package called elan?
Not in this flake.

But in nixpkgs.

Then its not our problem.

That documentation you linked doesn't say anything about the release candidates.

it tells me to run:

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

this link currently contains leanprover/lean4:v4.14.0-rc2 and contained leanprover/lean4:v4.13.0-rc3 a while ago when I started using Mathlib.

Use the Mathlib tag v4.13.0. The link you showed points to the tip of the master branch of Mathlib. It will always be very new.

[lenianiva]

I asked in https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/LSP.20Lake.20replaying.20dependencies/near/482705265. This might be unfixable. i.e. the Replay bit

From my limited understanding of Lean, the LSP needs to replay all dependency build files. Vide https://github.com/leanprover/lean4/blob/v4.12.0/src/lake/Lake/Build/Common.lean#L99

/--
Checks whether `info` is up-to-date, and runs `build` to recreate it if not.
If rebuilt, saves the new `depTrace` and build log to `traceFile`.
Returns whether `info` was already up-to-date.

**Up-to-date Checking**

If `traceFile` exists, checks that the hash in `depTrace` matches that
of the `traceFile`. If not, and old mode is enabled (e.g., `--old`), falls back
to the `oldTrace` modification time as the point of comparison.
If up-to-date, replay the build log stored in `traceFile`.

If `traceFile` does not exist, checks that `info` has a newer modification time
then `depTrace` / `oldTrace`. No log will be replayed.
-/
@[specialize] def buildUnlessUpToDate?
  [CheckExists ι] [GetMTime ι] (info : ι)
  (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
  (action : JobAction := .build) (oldTrace := depTrace.mtime)
: JobM Bool := do

[wuyoli]

That is not very specific. Could you pin down what behaviour is different?

the Replay doesn't happen with a .lake folder which I got via lake exe cache get

[lenianiva]

It may be because of this https://github.com/leanprover/lean4/blob/master/src/lake/README.md#augmenting-lakes-search-path

[lenianiva]

That is not very specific. Could you pin down what behaviour is different?

the Replay doesn't happen with a .lake folder which I got via lake exe cache get

Could you try adding pkgs.lean.lean-all to devShell? This would place lean and lake in the same path (please double check to be sure).

[wuyoli]

I had pkgs.lean.lean-all in there the whole time, because it is already in there in the template
and the binaries are in the same Directory:

$ which lean
/nix/store/r4f9dmyyyk73vs6isf6ar3rwksykw16m-lean-stage1/bin/lean
$ which lake
/nix/store/r4f9dmyyyk73vs6isf6ar3rwksykw16m-lean-stage1/bin/lake

[lenianiva]

I had pkgs.lean.lean-all in there the whole time, because it is already in there in the template and the binaries are in the same Directory:

$ which lean
/nix/store/r4f9dmyyyk73vs6isf6ar3rwksykw16m-lean-stage1/bin/lean
$ which lake
/nix/store/r4f9dmyyyk73vs6isf6ar3rwksykw16m-lean-stage1/bin/lake

Then I don't know how to solve this issue

[lenianiva]

I found a possible solution to your problem. If you build mathlib with this flake, and set this variable in your devShell:

            LEAN_PATH = "${mathlib.modRoot}";

This will expose the compiled module root to Lean LSP and it should probably start faster.