Closed RexWzh closed 1 month ago
LGTM, Thank you @RexWzh .
Is there a particular reason the env variables are called PORT
and CLIENT_PORT
, or could they be prefixed with e.g. LEAN4GAME_
in the future?
LGTM, Thank you @RexWzh .
Is there a particular reason the env variables are called
PORT
andCLIENT_PORT
, or could they be prefixed with e.g.LEAN4GAME_
in the future?
Thanks for the reply ;)
The variable PORT
is compatible with the code in index.mjs
and npm_scripts.md
Considering the script in package.json
:
"start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")",
"start_client": "cross-env NODE_ENV=development vite --host",
It is appropriate to use names like SERVER_PORT
or CLIENT_PORT
.
Thanks for the awesome project! I'm working on deploying a game myself and encountered a bug related to port configuration. I've made a small change to fix it.
Description: This PR updates the Vite server configuration to allow the setting of the client port using the environment variable
CLIENT_PORT
, with a default value of 3000. Additionally, it fixes a bug related to thebackendPort
configuration.The code here:
https://github.com/leanprover-community/lean4game/blob/4ed0753bb06b12437152a6e1ebf2b55774878fe8/vite.config.ts#L38
Can results in the following error:
Changes:
vite.config.js
to read theCLIENT_PORT
environment variable for the client port.backendPort
configuration.Benefits: