Add react_i18n

.gitignore

@@ -3,3 +3,4 @@ client/dist
 games/
 server/.lake
 **/.DS_Store
+/.lake

Lean4game/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

client/src/components/landing_page.tsx

@@ -1,5 +1,6 @@
 import * as React from 'react';
 import { useNavigate, Link } from "react-router-dom";
+import { useTranslation } from 'react-i18next';
 
 import '@fontsource/roboto/300.css';
 import '@fontsource/roboto/400.css';
@@ -138,14 +139,20 @@ function LandingPage() {
     "trequetrum/lean4game-logic",
   ]
   let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
+  const { t, i18n } = useTranslation();
 
   return <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
       <nav>
         <GithubIcon url="https://github.com/leanprover-community/lean4game"/>
       </nav>
+      <div>
+      <button onClick={() => i18n.changeLanguage("en")}>{flag["English"]}</button>
+      <button onClick={() => i18n.changeLanguage("fr")}>{flag["French"]}</button>
+      {/* Add more buttons for other languages as needed */}
+    </div>
       <div id="main-title">
-        <h1>Lean Game Server</h1>
+        <h1>{t("Lean Game Server")}</h1>
         <p>
           A repository of learning games for the
           proof assistant <a target="_blank" href="https://leanprover-community.github.io/">Lean</a> <i>(Lean 4)</i> and

client/src/i18n.ts

@@ -0,0 +1,36 @@
+import i18n from "i18next";
+import { initReactI18next } from "react-i18next";
+
+// the translations
+// (tip move them in a JSON file and import them,
+// or even better, manage them separated from your code: https://react.i18next.com/guides/multiple-translation-files)
+const resources = {
+  en: {
+    translation: {
+      "Welcome to React": "Welcome to React and react-i18next",
+      "Lean Game Server": "Lean Game Server translated"
+
+    }
+  },
+  fr: {
+    translation: {
+      "Welcome to React": "Bienvenue à React et react-i18next",
+      "Lean Game Server": "Lean Game Server French"
+    }
+  }
+};
+
+i18n
+.use(initReactI18next) // passes i18n down to react-i18next
+.init({
+    resources,
+    lng: "en", // language to use, more information here: https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
+    // you can use the i18n.changeLanguage function to change the language manually: https://www.i18next.com/overview/api#changelanguage
+    // if you're using a language detector, do not define the lng option
+
+    interpolation: {
+      escapeValue: false // react already safes from xss
+    }
+  });
+
+  export default i18n;

client/src/index.tsx

@@ -9,6 +9,7 @@ import ErrorPage from './components/error_page'
 import Welcome from './components/welcome'
 import LandingPage from './components/landing_page'
 import Level from './components/level'
+import './i18n';
 
 
 

package-lock.json

@@ -30,12 +30,14 @@
         "cytoscape-klay": "^3.1.4",
         "debounce": "^1.2.1",
         "express": "^4.18.2",
+        "i18next": "^23.10.1",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
         "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
         "octokit": "^3.1.2",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
+        "react-i18next": "^14.1.0",
         "react-markdown": "^8.0.4",
         "react-native": "^0.72.3",
         "react-redux": "^8.0.5",
@@ -8554,6 +8556,14 @@
         }
       ]
     },
+    "node_modules/html-parse-stringify": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/html-parse-stringify/-/html-parse-stringify-3.0.1.tgz",
+      "integrity": "sha512-KknJ50kTInJ7qIScF3jeaFRpMpE8/lfiTdzf/twXyPBLAGrLRTmkz3AdTnKeh40X8k9L2fdYwEp/42WGXIRGcg==",
+      "dependencies": {
+        "void-elements": "3.1.0"
+      }
+    },
     "node_modules/htmlparser2": {
       "version": "8.0.2",
       "resolved": "https://registry.npmjs.org/htmlparser2/-/htmlparser2-8.0.2.tgz",
@@ -8609,6 +8619,28 @@
         "node": ">=10.17.0"
       }
     },
+    "node_modules/i18next": {
+      "version": "23.10.1",
+      "resolved": "https://registry.npmjs.org/i18next/-/i18next-23.10.1.tgz",
+      "integrity": "sha512-NDiIzFbcs3O9PXpfhkjyf7WdqFn5Vq6mhzhtkXzj51aOcNuPNcTwuYNuXCpHsanZGHlHKL35G7huoFeVic1hng==",
+      "funding": [
+        {
+          "type": "individual",
+          "url": "https://locize.com"
+        },
+        {
+          "type": "individual",
+          "url": "https://locize.com/i18next.html"
+        },
+        {
+          "type": "individual",
+          "url": "https://www.i18next.com/how-to/faq#i18next-is-awesome.-how-can-i-support-the-project"
+        }
+      ],
+      "dependencies": {
+        "@babel/runtime": "^7.23.2"
+      }
+    },
     "node_modules/iconv-lite": {
       "version": "0.4.24",
       "resolved": "https://registry.npmjs.org/iconv-lite/-/iconv-lite-0.4.24.tgz",
@@ -13130,6 +13162,27 @@
       "resolved": "https://registry.npmjs.org/react-fast-compare/-/react-fast-compare-3.2.2.tgz",
       "integrity": "sha512-nsO+KSNgo1SbJqJEYRE9ERzo7YtYbou/OqjSQKxV7jcKox7+usiUVZOAC+XnDOABXggQTno0Y1CpVnuWEc1boQ=="
     },
+    "node_modules/react-i18next": {
+      "version": "14.1.0",
+      "resolved": "https://registry.npmjs.org/react-i18next/-/react-i18next-14.1.0.tgz",
+      "integrity": "sha512-3KwX6LHpbvGQ+sBEntjV4sYW3Zovjjl3fpoHbUwSgFHf0uRBcbeCBLR5al6ikncI5+W0EFb71QXZmfop+J6NrQ==",
+      "dependencies": {
+        "@babel/runtime": "^7.23.9",
+        "html-parse-stringify": "^3.0.1"
+      },
+      "peerDependencies": {
+        "i18next": ">= 23.2.3",
+        "react": ">= 16.8.0"
+      },
+      "peerDependenciesMeta": {
+        "react-dom": {
+          "optional": true
+        },
+        "react-native": {
+          "optional": true
+        }
+      }
+    },
     "node_modules/react-is": {
       "version": "18.2.0",
       "resolved": "https://registry.npmjs.org/react-is/-/react-is-18.2.0.tgz",
@@ -15469,6 +15522,14 @@
       "resolved": "https://registry.npmjs.org/vlq/-/vlq-1.0.1.tgz",
       "integrity": "sha512-gQpnTgkubC6hQgdIcRdYGDSDc+SaujOdyesZQMv6JlfQee/9Mp0Qhnys6WxDWvQnL5WZdT7o2Ul187aSt0Rq+w=="
     },
+    "node_modules/void-elements": {
+      "version": "3.1.0",
+      "resolved": "https://registry.npmjs.org/void-elements/-/void-elements-3.1.0.tgz",
+      "integrity": "sha512-Dhxzh5HZuiHQhbvTW9AMetFfBHDMYpo23Uo9btPXgdYP+3T5S+p+jgNy7spra+veYhBP2dCSgxR/i2Y02h5/6w==",
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
     "node_modules/vscode": {
       "name": "@codingame/monaco-vscode-api",
       "version": "1.69.13",

package.json

@@ -27,12 +27,14 @@
     "cytoscape-klay": "^3.1.4",
     "debounce": "^1.2.1",
     "express": "^4.18.2",
+    "i18next": "^23.10.1",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
     "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
     "octokit": "^3.1.2",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",
+    "react-i18next": "^14.1.0",
     "react-markdown": "^8.0.4",
     "react-native": "^0.72.3",
     "react-redux": "^8.0.5",