Updating to 4.16.0-rc1

Stream: general

[Asei Inoue]

Since updating to v4.16.0-rc1, I've been getting the following warning message:

❯ lake exe cache get
ℹ [10/10] Replayed cache
info: stderr: clang: warning: argument unused during compilation: '-static-libgcc' [-Wunused-command-line-argument]

This is causing my CI on Windows to fail. Could you please make it so that this warning doesn't appear?

see: CI log https://github.com/lean-ja/lean-by-example/actions/runs/12642701688/job/35227476047

[Edward van de Meent]

there's a bunch of talk about this in #mathlib4 > lake exe cache get error

[Asei Inoue]

updating Mathlib will solve error?

[Eric Wieser]

No, but you can stick with 4.15.0 until the issue is fixed upstream in a lean rc

[Asei Inoue]

which issue does track this problem?

[Asei Inoue]

@Eric Wieser

using v4.15.0 does not resolve the issue

lean-by-example on  main [$] took 43s
❯ cat .\lean-toolchain
leanprover/lean4:v4.15.0

lean-by-example on  main [$]
❯ lake exe cache get
✖ [6/10] Building Cache.Main:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [7/10] Building Cache.IO:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [8/10] Building Cache.Hashing:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [9/10] Building Cache.Requests:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- Cache.Main:c.o
- Cache.IO:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o
error: build failed

[Eric Wieser]

Try deleting .lake

[Asei Inoue]

I have removed .lake and tried lake exe cache get many times. Deleting .lake does not resolve the issue.

[Eric Wieser]

Have you also pinned mathlib to 4.15.0?

[Asei Inoue]

no. I will try.

[Asei Inoue]

failed. (pin mathlib to v4.15.0 and remove .lake and run lake update)

lean-by-example on  main [$!] took 39s
❯ lake update
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision '9837ca9d65d9de6fad1ef4381750ca688774e608'
info: mdgen: cloning https://github.com/Seasawher/mdgen
info: mdgen: checking out revision '0ca20e8b0f3eafdb3b9e6a67d65af50e79e6f730'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2c57364ef83406ea86d0f78ce3e342079a2fece5'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '9a0b533c2fbd6195df067630be18e11e4349051c'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '2689851f387bb2cef351e6825fe94a56a304ca13'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f0c584bcb14c5adfb53079781eeea75b26ebbd32'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'e8dc5fc16c625fc4fe08f42d625523275ddbbb4b'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
info: mathlib: running post-update hooks
✖ [4/10] Building Cache.IO:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\IO.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [6/10] Building Cache.Hashing:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Hashing.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [8/10] Building Cache.Requests:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Requests.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
✖ [9/10] Building Cache.Main:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe -c -o .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c.o.noexport .\.\.lake/packages\mathlib\.lake\build\ir\Cache\Main.c -O3 -DNDEBUG
info: stderr:
uncaught exception: no such file or directory (error code: 2)
error: external command 'c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.15.0\bin\leanc.exe' exited with code 1
Some required builds logged failures:
- Cache.IO:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o
- Cache.Main:c.o
error: build failed
error: mathlib: failed to fetch cache

[Asei Inoue]

should I uninstall and reinstall Lean itself?

[Eric Wieser]

That would be my next guess

[Asei Inoue]

remove .elan?

[Sebastian Ullrich]

yes

[Asei Inoue]

reinstall elan solves the issue!!!

[Kevin Buzzard]

Huh, this is quite rare. In the early days of lean 4 "delete .lake and try again" was a common fix for problems, but my impression is that it's now far less common that one needs to do this. On the other hand "delete .elan and try again" has always been vanishingly rare. I wonder what you did to trigger this?

[Asei Inoue]

I don’t know why…
I have just updated Lean and mathlib to v4.16.0-rc1…

[Sebastian Ullrich]

Could have been an older elan with fewer download integrity checks?