lean 4.7.0 failure on new mac

Stream: general

[Kevin Buzzard]

I just tried to create a new Lean game following instructions here; I used the game skeleton template to make a new repo, cloned it locally and typed lake update -R && lake build and I got the following error:

% lake update -R && lake build
info: downloading https://releases.lean-lang.org/lean4/v4.7.0/lean-4.7.0-darwin_aarch64.tar.zst
Total: 159.3 MiB Speed:  14.1 MiB/s
info: installing /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0
GameServer: cloning https://github.com/leanprover-community/lean4game.git to './.lake/packages/GameServer'
std: cloning https://github.com/leanprover/std4.git to './.lake/packages/std'
i18n: cloning https://github.com/hhu-adam/lean-i18n.git to './.lake/packages/i18n'
importGraph: cloning https://github.com/leanprover-community/import-graph to './.lake/packages/importGraph'
Cli: cloning https://github.com/mhuisi/lean4-cli to './.lake/packages/Cli'
warning: Cli: ignoring missing dependency manifest './.lake/packages/Cli/lake-manifest.json'
GameServer: running post-update hooks
[0/18] Building GameServer.Utils
[0/18] Building GameServer.Graph
[0/23] Building GameServer.Structures
[0/23] Compiling time.cpp
[0/37] Building Std.Tactic.OpenPrivate
[0/41] Building GameServer.Tactic.LetIntros
[0/74] Building GameServer.Options
[1/74] Compiling GameServer.Tactic.LetIntros
[2/74] Compiling Std.Tactic.OpenPrivate
[2/74] Building GameServer.Helpers.PrettyPrinter
[2/74] Building GameServer.ImportModules
[3/74] Compiling GameServer.ImportModules
[4/74] Compiling GameServer.Structures
[4/74] Building GameServer.InteractiveGoal
[5/74] Compiling GameServer.Options
[6/74] Compiling GameServer.InteractiveGoal
[7/74] Compiling GameServer.Graph
[8/74] Compiling GameServer.Utils
[8/74] Building GameServer.AbstractCtx
[9/74] Compiling GameServer.AbstractCtx
[9/74] Building GameServer.Hints
[10/74] Compiling GameServer.Helpers.PrettyPrinter
[10/74] Building GameServer.Helpers
[11/74] Building GameServer.EnvExtensions
[11/74] Compiling GameServer.Hints
[12/74] Compiling GameServer.Helpers
[22/74] Building GameServer.Inventory
[22/74] Compiling GameServer.EnvExtensions
[25/74] Compiling GameServer.Inventory
[26/74] Creating libleanTime.a
[27/74] Linking libleanTime.dylib
[28/74] Building Time.Basic
[28/74] Building I18n.Language
[28/74] Building I18n.Utils
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/i18n/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/packages/GameServer/server/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/i18n/.lake/build/lib:./.lake/packages/i18n/.lake/build/lib /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean ./.lake/packages/i18n/././I18n/Utils.lean -R ./.lake/packages/i18n/./. -o ./.lake/packages/i18n/.lake/build/lib/I18n/Utils.olean -i ./.lake/packages/i18n/.lake/build/lib/I18n/Utils.ilean -c ./.lake/packages/i18n/.lake/build/ir/I18n/Utils.c --load-dynlib=./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib, 0x0009): tried: './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/lib/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/lib/lean/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/usr/lib/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file, not in dyld cache), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/Users/buzzard/Lean/Projects/SquareRootOfTwo/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/buzzard/Lean/Projects/SquareRootOfTwo/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/Lean/Projects/SquareRootOfTwo/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)

(and then several more errors). What am I doing wrong?

[Kevin Buzzard]

Further analysis shows that this is not the fault of the game skeleton -- I cannot even get lean4game working on my mac laptop (Sequoia 15.5). npm install works fine but when I run npm start to start the server I get the same error:

[client]   ➜  Local:   http://localhost:3000/
[client]   ➜  Network: http://192.0.0.2:3000/
[client]   ➜  Network: http://100.64.0.1:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[server] error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/i18n/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/i18n/.lake/build/lib:./.lake/packages/i18n/.lake/build/lib /Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean ./.lake/packages/i18n/././time/Time/Basic.lean -R ./.lake/packages/i18n/././time -o ./.lake/packages/i18n/.lake/build/lib/Time/Basic.olean -i ./.lake/packages/i18n/.lake/build/lib/Time/Basic.ilean -c ./.lake/packages/i18n/.lake/build/ir/Time/Basic.c --load-dynlib=./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib
[server] error: stderr:
[server] libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib, 0x0009): tried: './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/lib/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/lib/lean/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/usr/lib/./.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file, not in dyld cache), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), './.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/Users/buzzard/Lean/Projects/lean4game/server/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/buzzard/Lean/Projects/lean4game/server/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (no such file), '/Users/buzzard/Lean/Projects/lean4game/server/.lake/packages/i18n/.lake/build/lib/libleanTime.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)
[server] error: external command `/Users/buzzard/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean` exited with code 134

I also cannot compile NNG4 on this machine -- same error. Compiling mathlib/FLT etc works fine. Any ideas on how to debug?

[Sebastian Ullrich]

You need a newer Lean version, that is the only fix

[Kevin Buzzard]

So I cannot do game development on my new mac right now? Wow. What's the minimum version of Lean that I need to pester @Alexander Bentkamp to bump lean4game to before I can supervise this summer student that I've just taken on, on how to make a Lean game?

[Sebastian Ullrich]

Yep, not much we can do to foresee future operating system versions breaking things unfortunately. You need 4.20.0+.

[Shreyas Srinivas]

Kevin Buzzard said:

So I cannot do game development on my new mac right now? Wow. What's the minimum version of Lean that I need to pester Alexander Bentkamp to bump lean4game to before I can supervise this summer student on how to make a Lean game?

You can do this yourself on a fork

[David Thrane Christiansen]

@Kevin Buzzard I've been able to get rid of similar issues with old Lean on new Mac OS by disabling precompiled modules. Upgrading your Lean version is by far the better approach, but if that can't happen, then this might be a workaround.

[Alexander Bentkamp]

I have just updated lean4game to v4.21.0. Its not yet live, but you should be able to use it locally already.

[Alexander Bentkamp]

GameSkeleton has not yet been updated. Jon created a bump-v4.21.0 branch. I am not sure whether its working.

[Dan Velleman]

Does this mean that other games on the game server will need to be updated?

[Kevin Buzzard]

A more precise question: if the maintainer of a game hosted by adam.math.hhu.de decides to add new material but not bump the repo to the latest Lean, will the deployment of the new version to the website still work?

[Alexander Bentkamp]

No, nobody will be forced to update, and yes, you will be able to add new material while using old lean versions.

[Alexander Bentkamp]

Ok, the bump-v4.21.0 of GameSkeleton works. And the adam.math.hhu.de will probably be updated on Monday.

[Kevin Buzzard]

Thanks so much for your prompt action! I had a two-week summer project thrown into temporary chaos by this!

[Alexander Bentkamp]

The update is live on adam.math.hhu.de now, by the way.

[Kevin Buzzard]

Thanks! An update from my side: I managed to bump both the server and my game repo to 4.21 and can compile it locally, but CI on my game repo is failing with the attached error.

Screenshot 2025-08-08 at 12.10.51.png

Any ideas? I thought I had made all the changes which were made on the skeleton.

[Alexander Bentkamp]

https://github.com/hhu-adam/GameSkeleton/commit/be14d11d65be7601c613036ae455ce6553a82803

[Alexander Bentkamp]

Maybe this change was made only after you checked.

[Jon Eugster]

Yep that's one of the slightly subideal things about that setup. There are several meta-/config-/...-files which need to be copy-pasted from the GameSkeleton into your own game. Anything under .github/ and potential fixes in the lakefile.lean are only two examples.

Btw @Kevin Buzzard, NNG is already bumped but I'd like to only deploy it to the server once we've tested some more for potential bugs.

[Kevin Buzzard]

CI is passing on my game repo now, thanks all!