lake exec cache get not working?

Stream: new members

[Lauri Oksanen]

When I run

lake +leanprover-community/mathlib4:lean-toolchain new test math && cd test
lake exe cache get
echo 'import Mathlib' > Test/Basic.lean
lake build

it seems that mathlib is starts to recompile. If I understand correctly the documentation

Using mathlib4 as a dependency

this shouldn't be the case, and the last command should be fast.

If I run the above without the build command, and open Basic.lean in Vscode, I get the message

Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.

Clicking "Restart File" seems to start recompilation of mathlib.

I can run codes from The Mechanics of Proof without issues. I am using

elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

lake --version
Lake version 5.0.0-0c9a488 (Lean version 4.16.0-rc1)

[Ruben Van de Velde]

Yes, this is unfortunately a known bug that should be fixed next week

[Ruben Van de Velde]

The workaround is to stick to lean 4.15

[Lauri Oksanen]

Thanks for the quick reply! I suppose that I need to change the first command to get 4.15 version. Would you be able to give me the correct command?

[Mauricio Collares]

Edit your lakefile.toml so that the mathlib part looks like this:

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

and then run lake update