Struggling to run games locally manually #254

ndcroos · 2024-07-28T22:53:31Z

I have tried to run NNG4 and GameSkeleton locally manually using the main branch of lean4game, but I get the following error when I try to access the game via the browser. I've tried to change my firewall settings, but I get the same result.

$ npm start

> [email protected] start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client"

(node:16020) [DEP0060] DeprecationWarning: The `util._extend` API is deprecated. Please use Object.assign() instead.
(Use `node --trace-deprecation ...` to show where the warning was created)
[client]
[client] > [email protected] start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server]
[server] > [email protected] start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client]   VITE v4.5.3  ready in 57000 ms
[client]
[client]   ➜  Local:   http://localhost:3000/
[client]   ➜  Network: http://172.20.224.1:3000/
[client]   ➜  Network: http://192.168.1.60:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[client] (node:15260) [DEP0060] DeprecationWarning: The `util._extend` API is deprecated. Please use Object.assign() instead.
[client] (Use `node --trace-deprecation ...` to show where the warning was created)
[client] 00:26:44 [vite] http proxy error at /data/g/local/NNG4/game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:44 [vite] http proxy error at /data/g/local/NNG4/inventory.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:44 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:49 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:49 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:49 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:49 [vite] http proxy error at /i18n/g/trequetrum/lean4game-logic/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /i18n/g/trequetrum/lean4game-logic/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /data/g/hhu-adam/robo/game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /data/g/leanprover-community/nng4/game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /data/g/djvelleman/stg4/game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:51 [vite] http proxy error at /data/g/trequetrum/lean4game-logic/game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:52 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:52 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:52 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:52 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:52 [vite] http proxy error at /i18n/g/trequetrum/lean4game-logic/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:53 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:54 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:54 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:54 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:54 [vite] http proxy error at /i18n/g/trequetrum/lean4game-logic/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:55 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:57 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:57 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:57 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:57 [vite] http proxy error at /i18n/g/trequetrum/lean4game-logic/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:26:58 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:27:03 [vite] http proxy error at /i18n/g/local/NNG4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:27:04 [vite] http proxy error at /i18n/g/leanprover-community/nng4/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:27:04 [vite] http proxy error at /i18n/g/hhu-adam/robo/en/Game.json:
[client] AggregateError [ECONNREFUSED]:
[client]     at internalConnectMultiple (node:net:1118:18)
[client]     at afterConnectMultiple (node:net:1685:7)
[client] 00:27:04 [vite] http proxy error at /i18n/g/djvelleman/stg4/en/Game.json:

This is how the game looks like in the browser window:

The text was updated successfully, but these errors were encountered:

joneugster · 2024-07-31T15:51:08Z

can you try what happens if you access localhost:3000/#/g/local/NNG4 instead? Note the local in there. And NNG4 is the case-sensitive folder name at lean4game/../NNG4 where you have called lake build to build the game.

Do you get the same?

Also once you get these AggregationErrors, you might have to restart npm start, it might not recover by itself.

(last note that lean4game:dev branch is incompatible with the NNG4 currently, might nees to use the main branch)

ndcroos · 2024-08-01T14:55:24Z

Thanks for getting back to me. I get the same results using the main branch. I think I might try to work on other issues for a while that don't require running the game locally.

ndcroos · 2024-08-02T18:32:20Z

I also get this error:

/lean4game (dev)
$ npm start

> [email protected] start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client"

(node:12244) [DEP0060] DeprecationWarning: The `util._extend` API is deprecated. Please use Object.assign() instead.
(Use `node --trace-deprecation ...` to show where the warning was created)
[server]
[server] > [email protected] start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client] > [email protected] start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[client]
[client]   VITE v4.5.3  ready in 27986 ms
[client]
[client]   ➜  Local:   http://localhost:3000/
[client]   ➜  Network: http://172.20.224.1:3000/
[client]   ➜  Network: http://192.168.1.60:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[server] error: > c:\Users\desti\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe -o .\.lake\build\bin\gameserver.exe .\.lake\build\ir\GameServer.c.o .\.lake\build\ir\GameServer\Utils.c.o .\.lake\build\ir\GameServer\AbstractCtx.c.o .\.lake\build\ir\GameServer\Graph.c.o .\.lake\build\ir\GameServer\Hints.c.o .\.lake\build\ir\GameServer\EnvExtensions.c.o .\.lake\build\ir\GameServer\Structures.c.o .\.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\build\ir\GameServer\RpcHandlers.c.o .\.lake\build\ir\GameServer\Game.c.o .\.lake/packages\std\.lake\build\ir\Std\Tactic\OpenPrivate.c.o .\.lake\build\ir\GameServer\ImportModules.c.o .\.lake\build\ir\GameServer\SaveData.c.o .\.lake\build\ir\GameServer\Tactic\LetIntros.c.o .\.lake\build\ir\GameServer\FileWorker.c.o .\.lake\build\ir\GameServer\Helpers\PrettyPrinter.c.o .\.lake\build\ir\GameServer\Helpers.c.o .\.lake\build\ir\GameServer\Inventory.c.o .\.lake\build\ir\GameServer\Options.c.o .\.lake\build\ir\GameServer\Commands.c.o .\.lake/packages\i18n\.lake\build\lib\leanTime.a
[server] error: stderr:
[server] ld.lld: error: too many exported symbols (got 69494, max 65535)
[server] clang: error: linker command failed with exit code 1 (use -v to see invocation)
[server] error: external command `c:\Users\desti\.elan\toolchains\leanprover--lean4---v4.7.0\bin\leanc.exe` exited with code 1
[server] [74/74] Linking gameserver.exe
[server] npm run start_server exited with code 1
[client] Terminate batch job (Y/N)?

This is the same error when I try this:

 ~/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: running post-update hooks
[74/74] Linking gameserver.exe

I think the issue is there, but I haven't been able to resolve this yet.

RexWzh · 2024-08-17T15:17:34Z

Hi @ndcroos , you might try to deploy a simple game first. Note that NNG4 requires mathlib as a dependency, which will need a stable internet connection.

Steps to Deploy Games:

Install Node.js:

curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.3/install.sh | bash
nvm install node && nvm use node

Clone and Build Game Template:

git clone https://github.com/hhu-adam/GameSkeleton.git
cd GameSkeleton
lake update -R
lake build

Set Up Lean4Game:

cd ..
git clone https://github.com/leanprover-community/lean4game.git
cd lean4game
npm install --force
# It is recommended to use 'tmux' to keep the session active
npm start

Visit your service at localhost:3000/#/g/local/GameSkeleton.

A demo example: https://lean4game.cubenlp.com/#/g/local/GameSkeleton

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Struggling to run games locally manually #254

Struggling to run games locally manually #254

ndcroos commented Jul 28, 2024

joneugster commented Jul 31, 2024

ndcroos commented Aug 1, 2024 •

edited

Loading

ndcroos commented Aug 2, 2024 •

edited

Loading

RexWzh commented Aug 17, 2024

Struggling to run games locally manually #254

Struggling to run games locally manually #254

Comments

ndcroos commented Jul 28, 2024

joneugster commented Jul 31, 2024

ndcroos commented Aug 1, 2024 • edited Loading

ndcroos commented Aug 2, 2024 • edited Loading

RexWzh commented Aug 17, 2024

Steps to Deploy Games:

ndcroos commented Aug 1, 2024 •

edited

Loading

ndcroos commented Aug 2, 2024 •

edited

Loading