lake update clone mathlib to wierd place

Stream: lean4

[MohanadAhmed]

Scott Morrison said:

Yes, that's correct, we currently require

• lake new blah math
• lake update
• lake exe cache get
• lake build
  Certainly we should incorporate lake update into lake new when called with math.
  I'm not sure about incorporating lake exe cache get, as it feels like that's something we want to teach new users about, to there's no harm in requiring it as a setup step.

If I follow the instructions above I notice that lake update clones mathlib to a weird location with a numerical name lake-packages\3651603622586474826. Then lake exe cache get clones it to the "correct" location. The project still works but I am guessing this is a bug somewhere inside lake update. I am on Windows with MinGB bash shell. (The behaviour is the same with Powershell also)

The log is shown below:

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage
$ lake new Demo math
info: Downloading lean-toolchain

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage
$ cd Demo

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage/Demo (main)
$ lake update
cloning https://github.com/leanprover-community/mathlib4.git to .\lake-packages\3651603622586474826
cloning https://github.com/EdAyers/ProofWidgets4 to .\lake-packages\proofwidgets
cloning https://github.com/mhuisi/lean4-cli.git to .\lake-packages\Cli
cloning https://github.com/gebner/quote4 to .\lake-packages\Qq
cloning https://github.com/JLimperg/aesop to .\lake-packages\aesop
cloning https://github.com/leanprover/std4 to .\lake-packages\std

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage/Demo (main)
$ lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4.git to .\lake-packages\mathlib
info: Downloading proofwidgets/v0.0.13/windows-64.tar.gz
info: Unpacking proofwidgets/v0.0.13/windows-64.tar.gz
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: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Requests
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
No files to download
Decompressing 3630 file(s)
unpacked in 8960 ms

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage/Demo (main)
$ code .

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage/Demo (main)
$ lake build
[1/2] Building Demo

Mohanad@PC-KW-60881 MINGW64 /w/LeanStuff/garbage/Demo (main)
$

[Mauricio Collares]

The weird location is a Lake bug which was recently fixed (see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/100.20theorems.20list.20and.20undergrad.20targets/near/382376197). Mathlib will get this new fix when its Lean toolchain is updated.

[MohanadAhmed]

Thanks

[Scott Morrison]

This will be working again once #6414 is merged.