Zulip Chat Archive

Stream: new members

Topic: LEAN not loading

Răzvan Flavius Panda (Jan 29 2025 at 17:22):

I am trying to load in VSCode LEAN https://github.com/Trequetrum/lean4game-logic/blob/main/Game/Levels/IffTactic/L05.lean#L35-L126

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

After I press the button to restart file and rebuild VSCode just hangs forever. In task manager I see multiple lean.exe and a lake.exe

Any help would be appreciated.

Răzvan Flavius Panda (Jan 29 2025 at 17:59):

After running fetch matlib build cache now it is running with a progress indicator although very slowly.

Răzvan Flavius Panda (Jan 29 2025 at 18:05):

It's been stuck on [745/1973] Building Mathlib.Algebra.Order.Field.InjSurj for a very long time

Ruben Van de Velde (Jan 29 2025 at 18:56):

Once you've fetched the cache, there should be no more building of anything starting with Mathlib.

Ruben Van de Velde (Jan 29 2025 at 18:56):

If you see that, there's something wrong with the cache you should fix first

Răzvan Flavius Panda (Jan 29 2025 at 19:00):

It got totally stuck on [745/1973] Building Mathlib.Algebra.Order.Field.InjSurj so I stopped it.

Răzvan Flavius Panda (Jan 29 2025 at 19:01):

Now when I press restart file to rebuild the imports I am no longer getting any progress updates.

Răzvan Flavius Panda (Jan 29 2025 at 19:01):

I tried doing a clean and no luck, ends up with rebuilding the imports with no progress.

Răzvan Flavius Panda (Jan 29 2025 at 19:05):

Now rebuild imports is throwing an error:

c:\Users\freeman\.elan\toolchains\leanprover--lean4---v4.7.0\bin\lake.exe setup-file D:/Projects/lean4game-logic/Game/Levels/IffTactic/L05.lean Init Game.Metadata failed:

stderr:
info: [4/45] Compiling time.cpp
error: failed to execute c++: no such file or directory (error code: 2)

Răzvan Flavius Panda (Jan 29 2025 at 19:10):

After a clean and rebuild imports it throws:

c:\Users\freeman\.elan\toolchains\leanprover--lean4---v4.7.0\bin\lake.exe setup-file D:/Projects/lean4game-logic/Game/Levels/IffTactic/L05.lean Init Game.Metadata failed:

stderr:
info: [0/28] Building GameServer.Utils
info: [0/27] Building GameServer.Graph
info: [0/29] Building GameServer.Options
info: [1/32] Compiling time.cpp
info: [1/51] Building GameServer.Helpers.PrettyPrinter
info: [13/210] Building GameServer.Structures
error: failed to execute c++: no such file or directory (error code: 2)
info: [151/740] Building GameServer.Tactic.LetIntros
info: [1938/1973] Building GameServer.InteractiveGoal
info: [1939/1973] Building GameServer.AbstractCtx
info: [1940/1973] Building GameServer.Helpers
info: [1941/1973] Building GameServer.Hints
info: [1944/1973] Building GameServer.EnvExtensions
info: [1945/1973] Building GameServer.Inventory

Răzvan Flavius Panda (Jan 29 2025 at 19:30):

I tried reinstalling elan but got: error: could not create link from 'C:\Users\freeman\.elan\bin\elan.exe' to 'C:\Users\freeman\.elan\bin\lake.exe'

Răzvan Flavius Panda (Feb 03 2025 at 19:36):

https://stackoverflow.com/questions/79409799/lean-lake-error-failed-to-execute-c-no-such-file-or-directory-error-code

Kevin Buzzard (Feb 03 2025 at 20:25):

Here's what happens if I make a new directory test and then within it, run

git clone git@github.com:Trequetrum/lean4game-logic.git
cd lean4game-logic/
lake exe cache get
lake build

. I get this:

output

and now if I type code . I can open Game/Levels/IffTactic/L05.lean and it works fine for me. So probably the problem is at your end.

Try disabling your antivirus if you're on Windows, and then try running the commands which work for me: can you say where your output diverges from the output I posted? Also, how much RAM does your machine have?

Sebastian Ullrich (Feb 03 2025 at 20:28):

Most likely the game server simply isn't made to be compiled on Windows

Kevin Buzzard (Feb 03 2025 at 20:30):

To be clear, I did the above on Linux.

Răzvan Flavius Panda (Feb 03 2025 at 20:31):

Sebastian Ullrich said:

Most likely the game server simply isn't made to be compiled on Windows

oh no :(

Răzvan Flavius Panda (Feb 03 2025 at 20:32):

PS D:\Projects\test\lean4game-logic> lake exe cache get
info: GameServer: cloning https://github.com/leanprover-community/lean4game.git to '.\.lake/packages\GameServer'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.lake/packages\mathlib'
info: std: cloning https://github.com/leanprover/std4.git to '.\.lake/packages\std'
info: i18n: cloning https://github.com/hhu-adam/lean-i18n.git to '.\.lake/packages\i18n'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '.\.lake/packages\importGraph'
info: Cli: cloning https://github.com/mhuisi/lean4-cli to '.\.lake/packages\Cli'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '.\.lake/packages\Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '.\.lake/packages\aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.lake/packages\proofwidgets'
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Building Cache.Hashing
info: [2/9] Compiling Cache.IO
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Building Cache.Main
info: [5/9] Compiling Cache.Requests
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache.exe
No files to download
Decompressing 4359 file(s)
unpacked in 45788 ms
PS D:\Projects\test\lean4game-logic> lake build
[1/28] Building GameServer.Utils
[1/28] Building GameServer.Graph
[1/29] Building GameServer.Options
[2/39] Building GameServer.Helpers.PrettyPrinter
[2/41] Building GameServer.Tactic.LetIntros
[2/41] Building GameServer.Structures
[2/41] Compiling time.cpp
error: failed to execute `c++`: no such file or directory (error code: 2)
[1938/2072] Building GameServer.AbstractCtx
[1939/2072] Building GameServer.InteractiveGoal
[1940/2072] Building GameServer.Helpers
[1941/2072] Building GameServer.Hints
[1944/2072] Building GameServer.EnvExtensions
[1945/2072] Building GameServer.Inventory

Răzvan Flavius Panda (Feb 03 2025 at 20:32):

Same issue

Ruben Van de Velde (Feb 03 2025 at 20:34):

Well do you have a c++ compiler?

Răzvan Flavius Panda (Feb 03 2025 at 20:34):

No, but I thought that would be provided by LEAN/lake

Ruben Van de Velde (Feb 03 2025 at 20:46):

I would not expect that

Răzvan Flavius Panda (Feb 03 2025 at 20:53):

Installing a C++ compiler and lake build fixed it. Thank you very much :)

Arthur Paulino (Feb 03 2025 at 20:53):

Lean brings a C compiler with it, leanc:

λ leanc
Lean C compiler

A simple wrapper around a C compiler. Defaults to `/home/arthur/.elan/toolchains/leanprover--lean4---v4.16.0/bin/clang`,
which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
as-is to the wrapped compiler.

Interesting options:
* `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit
* `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit

Mauricio Collares (Feb 04 2025 at 13:04):

It does include a leanc wrapper and a bundled clang. leanc is meant for internal Lean use only. Lake stopped using it to compile user-supplied C code in lean4#6176, and I think you should use bundled clang directly if you're calling it yourself.

Sebastian Ullrich (Feb 04 2025 at 13:23):

I believe you should consider all of it internal

Arthur Paulino (Feb 04 2025 at 18:41):

Why is it added to the user's PATH though?

Sebastian Ullrich (Feb 04 2025 at 20:01):

Ah, that's probably from the old days of Makefile builds

Last updated: May 02 2025 at 03:31 UTC