Update Lean to leanprover/lean4:v4.7.0-rc2 with error: `too

Stream: general

[Asei Inoue]

I have made a tool called mk-exercise. The current Lean version of that project is leanprover/lean4:v4.5.0-rc1.

When I tried to update it to leanprover/lean4:v4.7.0-rc2 I got the following error.

❯ lake exe mk_exercise Test/Src Test/Out
info: [6/6] Linking mk_exercise.exe
error: > c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.7.0-rc2\bin\leanc.exe -o .\.lake\build\bin\mk_exercise.exe .\.lake\build\ir\MkExercise.c.o .\.lake\build\ir\MkExercise\Basic.c.o .\.lake\build\ir\MkExercise\Extract.c.o
error: stderr:
ld.lld: error: too many exported symbols (got 68214, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\11325\.elan\toolchains\leanprover--lean4---v4.7.0-rc2\bin\leanc.exe` exited with code 1

[Asei Inoue]

note: OS of my pc is Windows 11.

[Kim Morrison]

@Asei Inoue, would you mind trying a recently nightly, e.g 2024-03-19?

[Kim Morrison]

We have been working on this issue recently, and hope we finally have it sorted.

[Kim Morrison]

Since you have no dependencies hopefully it is easy to try out a nightly.

[Kim Morrison]

If it works, this will be in v4.8.0-rc1 in early April.

[Asei Inoue]

it doesn't work:

❯ lake exe mk_exercise Test/Src Test/Out
error: toolchain 'nightly' does not have the binary `C:\Users\11325\.elan\toolchains\nightly\bin\lake.exe`

mk-exercise on  main [!]
❯ elan toolchain install nightly
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2024-03-21
info: downloading component 'lean'
172.6 MiB / 172.6 MiB (100 %)  66.3 MiB/s ETA:   0 s
info: installing component 'lean'
error: could not remove 'toolchain directory' directory: 'C:\Users\11325\.elan\toolchains\nightly'
info: caused by: アクセスが拒否されました。 (os error 5) # Access denied.

[Asei Inoue]

Opening the terminal with administrator rights did not work. :(

[Asei Inoue]

Successfully updated the version of Lean. (I manually deleted the .elan/toolchains/nightly directory and tried again.)

However, it still does not work.

mk-exercise on  main [!]
❯ lean --version
Lean (version 4.8.0-nightly-2024-03-21, x86_64-w64-windows-gnu, commit 2c15cdda044e, Release)

mk-exercise on  main [!]
❯ lake exe mk_exercise Test/Src Test/Out
info: [0/6] Building MkExercise.Extract
info: [0/6] Building MkExercise.Basic
info: [1/6] Compiling MkExercise.Basic
info: [2/6] Compiling MkExercise.Extract
info: [2/6] Building MkExercise
info: [5/6] Compiling MkExercise
info: [6/6] Linking mk_exercise.exe
error: > c:\Users\11325\.elan\toolchains\nightly\bin\leanc.exe -o .\.lake\build\bin\mk_exercise.exe .\.lake\build\ir\MkExercise.c.o.noexport .\.lake\build\ir\MkExercise\Basic.c.o.export .\.lake\build\ir\MkExercise\Extract.c.o.export -leanshared
error: stderr:
ld.lld: error: undefined symbol: initialize_Lake
>>> referenced by .\.lake\build\ir\MkExercise\Basic.c.o.export:(initialize_MkExercise_Basic)
>>> referenced by .\.lake\build\ir\MkExercise\Extract.c.o.export:(initialize_MkExercise_Extract)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\11325\.elan\toolchains\nightly\bin\leanc.exe` exited with code 1

[Kim Morrison]

Can you delete your .lake directory and try again?

[Kim Morrison]

If that fails, please ping Mac Malone. :-)

[Sebastian Ullrich]

We're probably missing a -lLake linker flag in this supportInterpreter + import Lake edge case

[Sebastian Ullrich]

@Asei Inoue Are you actually making use of import Lake in your own code? It looks like a copy-paste mistake

[Asei Inoue]

If that fails, please ping Mac Malone. :-)

It failed.

# deleting  .lake directory

mk-exercise on  main [!]
❯ lake exe mk_exercise Test/Src Test/Out
info: [0/6] Building MkExercise.Basic
info: [0/6] Building MkExercise.Extract
info: [1/6] Compiling MkExercise.Basic
info: [2/6] Building MkExercise
info: [2/6] Compiling MkExercise.Extract
error: > LEAN_PATH=.\.lake\build\lib PATH c:\Users\11325\.elan\toolchains\nightly\bin\lean.exe .\.\.\MkExercise.lean -R .\.\. -o .\.lake\build\lib\MkExercise.olean -i .\.lake\build\lib\MkExercise.ilean -c .\.lake\build\ir\MkExercise.c
error: stdout:
.\.\.\MkExercise.lean:4:5: error: unknown namespace 'Lake'
.\.\.\MkExercise.lean:11:17: error: unknown identifier 'FilePath'
.\.\.\MkExercise.lean:12:18: error: unknown identifier 'FilePath'
error: external command `c:\Users\11325\.elan\toolchains\nightly\bin\lean.exe` exited with code 1

@Mac Malone I dont know how to fix this

[Mac Malone]

Sebastian Ullrich said:

We're probably missing a -lLake linker flag in this supportInterpreter + import Lake edge case

Yes, I believe the problem here is that Leanc's shared linker flags do not include a shared version of the Lake library. (We probably need a libLake_shared parralleling libInit_shared.(

[Sebastian Ullrich]

We don't even do that for Lake itself so I would start with linking the static Lake library we already have as suggested

[Asei Inoue]

Is there anything I can do? Should I give up upgrading Lean for a while?

[Sebastian Ullrich]

Why do you import Lake in your code, why do you set supportInterpreter? It doesn't look like you make use of either.

[Asei Inoue]

@Sebastian Ullrich If I delete both import Lake and supportInterpreter I still get an error.

see: https://github.com/Seasawher/mk-exercise/tree/update-lean

[Asei Inoue]

@Sebastian Ullrich sorry, I was wrong. Thanks.