lean4game missing i18next

Stream: general

[Kevin Buzzard]

i18next.png

What have I done? I'm trying to run a lean game locally with npm start.

buzzard@buster:~/lean-projects/lean4game$ npm start

> lean4-game@0.1.0 start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_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] > lean4-game@0.1.0 start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server] error: compiled configuration is invalid; run with '-R' to reconfigure
[server] npm run start_server exited with code 1
[client]
[client]   VITE v4.5.1  ready in 327 ms
[client]
[client]   ➜  Local:   http://localhost:3000/
[client]   ➜  Network: http://10.110.24.210:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[client] Failed to resolve import "i18next" from "client/src/i18n.ts". Does the file exist?
[client] Failed to resolve import "i18next" from "client/src/i18n.ts". Does the file exist?
[client] Failed to resolve import "react-i18next" from "client/src/components/landing_page.tsx". Does the file exist?
[client] Failed to resolve import "i18next" from "client/src/components/welcome.tsx". Does the file exist?
[client] Failed to resolve import "react-i18next" from "client/src/components/level.tsx". Does the file exist?
[client] Failed to resolve import "react-country-flag" from "client/src/components/popup/preferences.tsx". Does the file exist?

(etc etc)

My game builds locally, the lean-toolchain is 4.7.0 for both lean4game and my game, and I'm using mathlib commit a45ae63747140c1b2cbad9d46f518015c047047a (HEAD, tag: v4.7.0)

[Julian Berman]

That sounds like some dependencies aren't installed. Try npm i

[Kevin Buzzard]

Yeah you're right, I updated lean4game and then just typed npm start as usual, but I had to type npm installagain first. All fixed now! Thanks!

[Kevin Buzzard]

Oh, I tell a lie, I just get further but now a new error:

buzzard@buster:~/lean-projects/lean4game$ npm start

> lean4-game@0.1.0 start
> concurrently -n server,client -c blue,green "npm run start_server" "npm run start_client"

[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]
[server] error: compiled configuration is invalid; run with '-R' to reconfigure
[server] npm run start_server exited with code 1
[client]
[client]   VITE v4.5.3  ready in 340 ms
[client]
[client]   ➜  Local:   http://localhost:3000/
[client]   ➜  Network: http://10.110.24.210:3000/
[client] [vite-plugin-static-copy] Collected 7 items.
[client] 02:28:53 [vite] http proxy error at /i18n/g/local/FilterGame/en/Game.json:
[client] Error: connect ECONNREFUSED 127.0.0.1:8080
[client]     at TCPConnectWrap.afterConnect [as oncomplete] (node:net:1595:16)

[Julian Berman]

I would try doing what it says I think, if you haven't already. Namely running with -R. Now what command that is meant to be passed to... who knows. But try passing it to npm start, maybe as npm start -- -R and pray?

[Julian Berman]

(The end of that message seems to say that the frontend and backend of the app are disagreeing about what port the server is running on, which that configuration probably contains?)

[Kevin Buzzard]

So cd server then lake build -R has fixed it completely. Thanks so much Julian! I'm demoing this game in about 7 hours and I've not had any sleep yet :-)

[Julian Berman]

Hooray!