search

hhu-adam / GameSkeleton

The standard template to create a lean game
MIT License
15 stars 1 forks source link

windows11 vscode cannot “lake update -R” #2

Open langkong opened 1 week ago

langkong commented 1 week ago

PS C:\maker\lean4\gameskeleton> lake update -R warning: Cli: ignoring missing dependency manifest '..lake\packages\Cli\lake-manifest.json' GameServer: running post-update hooks [74/74] Linking gameserver.exe error: > c:\Users\54861.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\54861\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe exited with code 1 PS C:\maker\lean4\gameskeleton>

joneugster commented 1 week ago

I believe this might be the same error as this issue: https://github.com/leanprover-community/lean4game/issues/241

So that should hopefully be Windows specific and fixed once we get things updated to the newer version.