Error building NNG4

Stream: new members

[Nick Decroos]

Edit: I posted in the wrong stream. This topic should actually be in the new members stream.

When I try to build NNG4, I get the following error:

desti@DESKTOP-HAI6C7L MINGW64 ~/OneDrive/Documenten/NNG4 (main)
$ lake update -R
warning: Cli: ignoring missing dependency manifest '.\.lake\packages\Cli\lake-manifest.json'
warning: Qq: ignoring missing dependency manifest '.\.lake\packages\Qq\lake-manifest.json'
error: > c:\Users\desti\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe -o .\.lake\packages\GameServer\server\.lake\build\bin\gameserver.exe .\.lake\packages\GameServer\server\.lake\build\ir\GameServer.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Utils.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\AbstractCtx.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Graph.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Hints.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\EnvExtensions.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Structures.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\InteractiveGoal.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Utils.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\PO\Definition.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Language.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\EnvExtension.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\InterpolatedStr.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Json\Read.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Json\Write.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Json.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\PO\Read.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\PO\Write.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\PO.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Translate.c.o .\.lake\packages\i18n\.lake\build\ir\Time\Basic.c.o .\.lake\packages\i18n\.lake\build\ir\Time.c.o .\.lake\packages\i18n\.lake\build\ir\I18n\Template.c.o .\.lake\packages\i18n\.lake\build\ir\I18n.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\RpcHandlers.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Game.c.o .\.lake\packages\std\.lake\build\ir\Std\Tactic\OpenPrivate.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\ImportModules.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\SaveData.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Tactic\LetIntros.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\FileWorker.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Helpers\PrettyPrinter.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Helpers.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Inventory.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Options.c.o .\.lake\packages\GameServer\server\.lake\build\ir\GameServer\Commands.c.o .\.lake\packages\i18n\.lake\build\lib\leanTime.a
error: stderr:
ld.lld: error: too many exported symbols (got 69514, max 65535)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `c:\Users\desti\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe` exited with code 1
GameServer: updating repository '.\.lake\packages\GameServer' to revision '66aa8e688ec6d684bc2ad37c7eee46627a0481b2'
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.lake\packages\mathlib'
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'
Qq: cloning https://github.com/leanprover-community/quote4 to '.\.lake\packages\Qq'
aesop: cloning https://github.com/leanprover-community/aesop to '.\.lake\packages\aesop'
proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '.\.lake\packages\proofwidgets'
GameServer: running post-update hooks
[0/74] Compiling time.cpp
[0/74] Building GameServer.Utils
[0/74] Building GameServer.Graph
[0/74] Building GameServer.Structures
[2/74] Compiling GameServer.Structures
[2/74] Compiling GameServer.Graph
[2/74] Creating leanTime.a
[3/74] Building Std.Tactic.OpenPrivate
...

How can I resolve this?
I use windows 10.

$ lean -v
Lean (version 4.9.0, x86_64-w64-windows-gnu, commit 8f9843a4a5fe, Release)

[Jon Eugster]

Im not sure what this "clang: too many exported symbols" means and I haven't googled it yet, but there is a slight chance that this might be caused by the older version of lean-i18n using the FFI (foreign function interface) to use a function from the c++ standard library whiich somehow doesn't fully work on windows. If that was the case, hopefully updating nng to the newer version will solve this (I just removed the ffi use completely), but unfortunately I have been busy working on things and it'll still take a while until everything can be updated to the newest lean.

But maybe somebody how actual knows anything about c/c++ can be of more help

[Jon Eugster]

(here is the related issue with more details by @Nick Decroos : https://github.com/leanprover-community/lean4game/issues/254)

[Sebastian Ullrich]

This should be fixed in newer Lean versions than 4.7.0

[Notification Bot]

This topic was moved here from #general > Error building NNG4 by Kim Morrison.