Does math lib get built every time I open a .lean file?

Stream: new members

[Dominic Steinitz]

I just opened a .lean file the first line of which is import Mathlib and I see e.g. info: [1804/3689] Building Mathlib.ModelTheory.Encoding - this happened yesterday when I did the same thing. I guess I shouldn't have closed the file but I assumed that once Mathlib it was built it wouldn't get rebuilt? I should have said I am using emacs.

[Ruben Van de Velde]

It should not show any of that if you run lake exe cache get first

[Ruben Van de Velde]

Perhaps unless you're creating a binary output

[Dominic Steinitz]

I wondered if that might be the case.

[Dominic Steinitz]

Oh no - I ran lake exe cache get and opened a lean file and it started building mathlib :-(

[Ruben Van de Velde]

What was the output of lake exe cache get?

[Dominic Steinitz]

lake exe cache get
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
info: [5/9] Compiling Cache.Main
info: [9/9] Linking cache
info: stderr:
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 14.4.0, which is newer than target minimum of 14.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 14.4.0, which is newer than target minimum of 14.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 14.4.0, which is newer than target minimum of 14.0.0
leantar is too old; downloading more recent version
Attempting to download 3691 file(s)
Downloaded: 3691 file(s) [attempted 3691/3691 = 100%] (100% success)
Decompressing 3691 file(s)
unpacked in 3037 ms

[Dominic Steinitz]

I followed the instructions here: https://leanprover-community.github.io/install/macos.html but I don't seem to have VS Code(?) - did I miss a step? (I am abandoning emacs for now as everything seems to want you to use VS Code(?))

[Dominic Steinitz]

Hmm - maybe I have to logout and login again

[Dominic Steinitz]

But then all applications will get shut down :-(

[Dominic Steinitz]

code .
zsh: command not found: code

[Ruben Van de Velde]

Weird, that looks correct. And if you run lake build from the command line?

[Dominic Steinitz]

dom@Wandle lftcm2023 % lake build
[353/3747] Building LftCM.C11_Algebraic_Geometry.help
[353/3747] Building Projects.TestProject
stdout:
Hello World!
[569/3747] Building Projects
[1353/3747] Building LftCM.Attr
[1640/3747] Building LftCM.C02_Logic.Logic
...
error: external command `/Users/dom/.elan/toolchains/leanprover--lean4---v4.0.0-rc4/bin/lean` exited with code 1

[Dominic Steinitz]

Maybe I should try a different directory

[Dominic Steinitz]

Hmmm - it seems to be working in emacs now but I failed to get it working in VS

[Dominic Steinitz]

And excitingly the differential geometry example seems to be working and contains fibre bundles and Lie groups

[Dominic Steinitz]

Though bafflingly you seem to be able to define the n-sphere as a manifold without giving any charts but that question does not belong in this thread