search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

Struggling to run games locally manually #254

Open ndcroos opened 3 months ago

ndcroos commented 3 months ago

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

> lean4-game@0.1.0 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] > lean4-game@0.1.0 start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server]
[server] > lean4-game@0.1.0 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: lean4game

joneugster commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

I also get this error:

/lean4game (dev)
$ npm start

> lean4-game@0.1.0 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] > lean4-game@0.1.0 start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client] > lean4-game@0.1.0 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 commented 3 months ago

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:

  1. Install Node.js:

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

  2. Clone and Build Game Template:

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

  3. 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