lake serve running very long

Stream: new members

[toshi]

hello new user of lean4 here, im having trouble importing mathlib dependency. lakefile.toml:

name = "learning-lean"
# defaultTargets = [""]

[[lean_lib]]
name = "my-lean-lib"

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.22.0"

i ran lake exe cache get succesfully with .lake folder created but if i open neovim it is processing for very long and builds every thing from battery to mathlib; i think nvim.lean is running lake serve how should i troubleshoot?

many thanks
P.S. before i added dependency the nvim worked fine with infoview updating correctly
P.S. .lake/packages/mathlib is correct toolchain and .lake/packages/mathlib/.lake/build exist with cache
P.S. im on NixOS

[Julian Berman]

If you run lake build does it exit immediately or does it also build things?

[toshi]

i came back this morning and now its different behaviour:

• lake build: immediately done, Build completed succesfully
• lake exe cache get(!): error: unknown executable cache
• nvim: ```error:
  unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:```
i tried deleteing ~/.cache/mathlib to no avail, i also tried deleting .lake but since lake exe cache get doesnt work no .lake folder is generaeted :sad:

[Ruben Van de Velde]

Sounds like lake doesn't think you depend on mathlib

[Ruben Van de Velde]

Maybe run lake update before cache