From cb711205a2052eeee52b4aac74a11fcacd5648bd Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Thu, 21 Mar 2024 18:11:17 +0800 Subject: [PATCH 1/3] Add react_i18n --- .gitignore | 1 + Lean4game/Basic.lean | 1 + client/src/components/landing_page.tsx | 9 +++- client/src/i18n.ts | 36 +++++++++++++++ client/src/index.tsx | 1 + package-lock.json | 61 ++++++++++++++++++++++++++ package.json | 2 + 7 files changed, 110 insertions(+), 1 deletion(-) create mode 100644 Lean4game/Basic.lean create mode 100644 client/src/i18n.ts diff --git a/.gitignore b/.gitignore index f6fa519e..4644d2fb 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ client/dist games/ server/.lake **/.DS_Store +/.lake diff --git a/Lean4game/Basic.lean b/Lean4game/Basic.lean new file mode 100644 index 00000000..e99d3a6f --- /dev/null +++ b/Lean4game/Basic.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 12dba1bb..987e852f 100644 --- a/client/src/components/landing_page.tsx +++ b/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
+
+ + + {/* Add more buttons for other languages as needed */} +
-

Lean Game Server

+

{t("Lean Game Server")}

A repository of learning games for the proof assistant Lean (Lean 4) and diff --git a/client/src/i18n.ts b/client/src/i18n.ts new file mode 100644 index 00000000..b187c463 --- /dev/null +++ b/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; diff --git a/client/src/index.tsx b/client/src/index.tsx index 5fff5113..c36cd8dc 100644 --- a/client/src/index.tsx +++ b/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'; diff --git a/package-lock.json b/package-lock.json index ff05b9c1..8f2ad797 100644 --- a/package-lock.json +++ b/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", diff --git a/package.json b/package.json index 72053c4a..0c304fab 100644 --- a/package.json +++ b/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", From 64d7879c32be17e3c5727855b48da06b529063b1 Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Thu, 21 Mar 2024 18:13:31 +0800 Subject: [PATCH 2/3] delete accidently lake init --- Lean4game/Basic.lean | 1 - 1 file changed, 1 deletion(-) delete mode 100644 Lean4game/Basic.lean diff --git a/Lean4game/Basic.lean b/Lean4game/Basic.lean deleted file mode 100644 index e99d3a6f..00000000 --- a/Lean4game/Basic.lean +++ /dev/null @@ -1 +0,0 @@ -def hello := "world" \ No newline at end of file From 830bffaf1174170ba7dd4dc57182e6509eab657b Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Sat, 23 Mar 2024 09:07:30 +0800 Subject: [PATCH 3/3] Remove gitignore introduced by accidently lake init --- .gitignore | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitignore b/.gitignore index 4644d2fb..f6fa519e 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,3 @@ client/dist games/ server/.lake **/.DS_Store -/.lake