windows11 vscode cannot “lake update -R”

[langkong]

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]

I believe this might be the same error as this issue: leanprover-community/lean4game#241

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