From a15dd0a1bd3e4fb381042ef0b7bf8b75c55c24b9 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Apr 2024 11:23:27 +0200 Subject: [PATCH 01/12] bump i18n --- server/lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 92ef133..5210e4c 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -22,7 +22,7 @@ {"url": "https://github.com/hhu-adam/lean-i18n.git", "type": "git", "subDir": null, - "rev": "f193a3d02bbe96cafc462fcb54d5ca73374fd553", + "rev": "62dde5278a45771629f043e48effef44b4147ff8", "name": "i18n", "manifestFile": "lake-manifest.json", "inputRev": "main", From 67b03d9ccf36845b236a6519b3a9704217a0fd02 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Apr 2024 14:06:41 +0200 Subject: [PATCH 02/12] bump to v4.7.0 --- server/GameServer/RpcHandlers.lean | 1 - server/lake-manifest.json | 17 +++++++++++++---- server/lakefile.lean | 8 +++++--- server/lean-toolchain | 2 +- 4 files changed, 19 insertions(+), 9 deletions(-) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index 6ad1578..e81bce4 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -1,6 +1,5 @@ import GameServer.EnvExtensions import GameServer.InteractiveGoal -import Std.Data.Array.Init.Basic import GameServer.Hints import I18n diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 5210e4c..011a2fa 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", + "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "v4.7.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", @@ -22,10 +22,19 @@ {"url": "https://github.com/hhu-adam/lean-i18n.git", "type": "git", "subDir": null, - "rev": "62dde5278a45771629f043e48effef44b4147ff8", + "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39", "name": "i18n", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.7.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.7.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "GameServer", diff --git a/server/lakefile.lean b/server/lakefile.lean index 2fd0de9..bf56c16 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -4,11 +4,13 @@ open Lake DSL package GameServer -- Using this assumes that each dependency has a tag of the form `v4.X.0`. --- def leanVersion : String := s!"v{Lean.versionString}" -def leanVersion := "v4.6.0" -- TODO +def leanVersion : String := s!"v{Lean.versionString}" require std from git "https://github.com/leanprover/std4.git" @ leanVersion -require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ "main" -- leanVersion +require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion + +require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion + lean_lib GameServer diff --git a/server/lean-toolchain b/server/lean-toolchain index f96d662..9ad3040 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.1 +leanprover/lean4:v4.7.0 From 499bb00d4f6785ae4103d584337867a0c43656c1 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Apr 2024 14:43:30 +0200 Subject: [PATCH 03/12] fix language loading on landing page --- client/src/components/landing_page.tsx | 16 +++++----------- client/src/config.json | 1 - client/src/i18n.ts | 19 ++++++++++++------- 3 files changed, 17 insertions(+), 19 deletions(-) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 5178425..be12fc0 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -33,20 +33,12 @@ function GithubIcon({url='https://github.com'}) { } function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { - let { t, i18n } = useTranslation() + let { t } = useTranslation() let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); } - // we use this to reload the tile 1x after the translation is loaded. - let [loadedTranslation, setLoadedTranslation] = React.useState(false) - - // Load the namespace of the game - i18next.loadNamespaces(gameId).catch(err => { - console.warn(`translations for ${gameId} do not exist`) - }).then(() => {setLoadedTranslation(true)}) - if (typeof data === 'undefined') { return <> } @@ -105,8 +97,11 @@ function LandingPage() { const { t, i18n } = useTranslation() - let allTiles = lean4gameConfig.allGames.map((gameId) => { + // Load the namespaces of all games + // TODO: should `allGames` contain game-ids starting with `g/`? + i18next.loadNamespaces(lean4gameConfig.allGames.map(id => `g/${id}`)) + let allTiles = lean4gameConfig.allGames.map((gameId) => { let q = useGetGameInfoQuery({game: `g/${gameId}`}) // if (q.isError) { @@ -122,7 +117,6 @@ function LandingPage() { return q.data?.tile }) - return