unable to update Lean4 version to v4.8.0

Stream: lean4

[Asei Inoue]

I would like to update my repository below from v4.8.0-rc1 to v4.8.0.
https://github.com/Seasawher/mdgen/tree/main

but I get an following error:

mdgen on  issue26 [!]
❯ lake build --quiet
笨・[3/9] Building Mdgen.ConvertToMd:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Mdgen\ConvertToMd.c.o.noexport .\.\.lake\build\ir\Mdgen\ConvertToMd.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.8.0\bin\leanc.exe' exited with code 1
笨・[6/9] Building Mdgen.File:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Mdgen\File.c.o.noexport .\.\.lake\build\ir\Mdgen\File.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.8.0\bin\leanc.exe' exited with code 1
笨・[7/9] Building Mdgen.Main:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Mdgen\Main.c.o.noexport .\.\.lake\build\ir\Mdgen\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.8.0\bin\leanc.exe' exited with code 1
笨・[8/9] Building Mdgen:c.o
trace: .> c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Mdgen.c.o.noexport .\.\.lake\build\ir\Mdgen.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.8.0\bin\leanc.exe' exited with code 1
Some builds logged failures:
- Mdgen.ConvertToMd:c.o
- Mdgen.File:c.o
- Mdgen.Main:c.o
- Mdgen:c.o
error: build failed

[Asei Inoue]

what I tried:

• remove .lake directory and run lake build again

[Asei Inoue]

I cannot find any error when opening files in editor.

[Asei Inoue]

oh, I can update to v4.9.0-rc1 !! Is this a known issue?

[Asei Inoue]

I use Windows PC. Is there no error in Mac or Ubuntu?

[Asei Inoue]

The mdgen update is over, but this issue is still of interest to me.

[Amelia Livingston]

I get a similar error when trying to bump my mathlib :(

$ lake exe cache get
Γ£û [6/10] Building Cache.Main:c.o
trace: .> c:\Users\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Cache\Main.c.o.noexport
 .\.\.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\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe' exited with code 1
Γ£û [7/10] Building Cache.IO:c.o
trace: .> c:\Users\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Cache\IO.c.o.noexport .
\.\.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\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe' exited with code 1
Γ£û [8/10] Building Cache.Hashing:c.o
trace: .> c:\Users\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Cache\Hashing.c.o.noexp
ort .\.\.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\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe' exited with code 1
Γ£û [9/10] Building Cache.Requests:c.o
trace: .> c:\Users\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe -c -o .\.\.lake\build\ir\Cache\Requests.c.o.noex
port .\.\.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\amelia\.elan\toolchains\leanprover--lean4---v4.8.0\bin\leanc.exe' exited with code 1
Some builds logged failures:
- Cache.Main:c.o
- Cache.IO:c.o
- Cache.Hashing:c.o
- Cache.Requests:c.o
error: build failed

[Kim Morrison]

@Asei Inoue. could not reproduce via:

git clone git@github.com:Seasawher/mdgen.git
cd mdgen
lake build
echo leanprover/lean4:v4.8.0 > lean-toolchain
lake build

which worked without errors for me.

If you can find a repro that would be great.

[Kim Morrison]

@Amelia Livingston, there isn't enough detail in your message unfortunately for me to be able to try to reproduce.

[Kim Morrison]

Could you say which repo/commit you started from, and what commands you ran?

[Asei Inoue]

Oh, I think my issue is caused by Windows OS…?
The CI on ubuntu seems to be successful.
I will try to write CI on Windows.

[Mac Malone]

I looks to me like your v4.8.0 installation of Lean might be corrupted. Uninstalling it (e.g., via elan uninstall leanprover/lean4:v4.8.0) and reinstalling might help.

[Asei Inoue]

I found no error on another Windows machine. @Mac Malone Thanks.

[Amelia Livingston]

Sorry for the undetailed message - this was just on mathlib main, on commit cc4f996. But after pulling again this morning, lake exe cache get works fine, so I'm sorry for the noise.