diff --git a/README.md b/README.md
index 2661d9f..8d7680f 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
* Step 5: [How to Run Games Locally](doc/running_locally.md)
* Step 7: [How to Update an existing Game](doc/update_game.md)
-* Step 8: [How to Publishing a Game](doc/publish_game.md)
+* Step 9: [How to Publishing a Game](doc/publish_game.md)
* [Troubleshooting](doc/troubleshoot.md)
## Documentation
@@ -37,6 +37,17 @@ not fully written yet.
Contributions to `lean4game` are always welcome!
+### Translation
+
+The interface can be translated to various languages. For adding a translation, one needs to do the following:
+
+1. In `client/src/config.json`, add your new language. The "iso" key is the ISO language code, i.e. it should be accepted by "i18next" and "GNU gettext"; the "flag" key is once accepted by [react-country-flag](https://www.npmjs.com/package/react-country-flag).
+2. Run `npm run translate`. This should create a new file `client/public/locales/{language}/translation.json`. (alternatively you can copy-paste `client/public/locales/en/translation.json`)
+3. Add all translations.
+4. Commit the changes you made to `config.json` together with the new `translation.json`.
+
+For translating games, see [Translating a game](doc/translate.md).
+
## Security
Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
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
diff --git a/client/src/config.json b/client/src/config.json
index 2ff6f2c..9a4d059 100644
--- a/client/src/config.json
+++ b/client/src/config.json
@@ -3,7 +3,6 @@
"leanprover-community/nng4",
"hhu-adam/robo",
"djvelleman/stg4",
- "miguelmarco/stg4",
"trequetrum/lean4game-logic"
],
diff --git a/client/src/css/landing_page.css b/client/src/css/landing_page.css
index 7a06350..4831c9f 100644
--- a/client/src/css/landing_page.css
+++ b/client/src/css/landing_page.css
@@ -19,7 +19,7 @@ a {
@viewport {
width: device-width ;
- zoom: 1.0 ;
+ initial-scale: 1.0 ;
}
.landing-page {
diff --git a/client/src/i18n.ts b/client/src/i18n.ts
index a044abe..a2db8a8 100644
--- a/client/src/i18n.ts
+++ b/client/src/i18n.ts
@@ -3,13 +3,12 @@ import Backend from "i18next-http-backend"
import { initReactI18next } from "react-i18next";
i18n
-.use(initReactI18next) // passes i18n down to react-i18next
+.use(initReactI18next)
.use(Backend)
.init({
ns: ['translation'],
backend: {
- // see https://github.com/i18next/i18next-http-backend
-
+ // > see https://github.com/i18next/i18next-http-backend
loadPath: function(lngs, namespaces: Array) {
if (namespaces[0].startsWith("g/")) {
return '/i18n/{{ns}}/{{lng}}/Game.json';
@@ -18,12 +17,18 @@ i18n
}
}
},
- 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
+ // > language to use, more information here:
+ // > https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
+ lng: "en",
+ // we use natural language keys, so we don't need a fallback language.
+ fallbackLng: false,
+ // > 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
returnEmptyString: false,
interpolation: {
- escapeValue: false // react already safes from xss
+ // > react already safes from xss
+ escapeValue: false
}
});
diff --git a/doc/create_game.md b/doc/create_game.md
index 3a17fc0..589fc1d 100644
--- a/doc/create_game.md
+++ b/doc/create_game.md
@@ -242,7 +242,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
-## 8. Publish your game
+## 8. Add translation
+
+See [Translating a game](translate.md).
+
+## 9. Publish your game
To publish your game on the official server, see [Publishing a game](publish_game.md)
diff --git a/doc/translate.md b/doc/translate.md
new file mode 100644
index 0000000..a1484f8
--- /dev/null
+++ b/doc/translate.md
@@ -0,0 +1,30 @@
+# Translation
+
+The game server supports internationalisation ("i18n") using [lean-i18n](https://github.com/hhu-adam/lean-i18n) and [i18next](https://www.npmjs.com/package/i18next).
+
+The intended workflow currently is the following:
+
+1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
+2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
+4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
+5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
+
+If you choose the correct language in the "Preferences" of the game, you should see your translations.
+
+## Alternative: avoiding .po
+
+Note: This workflow is subject to change, and it might be that in future the server can directly read `.po` files. Until then, there is also an alternative workflow you might choose:
+
+0. Add `useJson: true` to `.i18n/config.json`
+1. `lake build` or `lake exe i18n --template` will now create a Json instead: `.i18n/en/Game.json`.
+2. Add translations to a copy of this Json an save it as `.i18n/{language}/Game.json`
+
+## Non-English games
+
+For games written in a language different than English, you should set the correct source language (`sourceLang`) in `.i18n/config.json`. Afterwards, on `lake build` the template should appear under the chosen language, and can be translated (e.g. into English) as described above.
+
+## New languages
+
+The server has a set number of languages one can select.
+If your game has been translated to a language not selectable, [open an issue at lean4game](https://github.com/leanprover-community/lean4game/issues) requesting this new language.
+Or, even better, create a PR to translate the [server interface](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales) into that new language.
diff --git a/package-lock.json b/package-lock.json
index 59359c6..f47b88e 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -6278,12 +6278,12 @@
}
},
"node_modules/body-parser": {
- "version": "1.20.1",
- "resolved": "https://registry.npmjs.org/body-parser/-/body-parser-1.20.1.tgz",
- "integrity": "sha512-jWi7abTbYwajOytWCQc37VulmWiRae5RyTpaCyDcS5/lMdtwSz5lOpDE67srw/HYe35f1z3fDQw+3txg7gNtWw==",
+ "version": "1.20.2",
+ "resolved": "https://registry.npmjs.org/body-parser/-/body-parser-1.20.2.tgz",
+ "integrity": "sha512-ml9pReCu3M61kGlqoTm2umSXTlRTuGTx0bfYj+uIUKKYycG5NtSbeetV3faSU6R7ajOPw0g/J1PvK4qNy7s5bA==",
"dependencies": {
"bytes": "3.1.2",
- "content-type": "~1.0.4",
+ "content-type": "~1.0.5",
"debug": "2.6.9",
"depd": "2.0.0",
"destroy": "1.2.0",
@@ -6291,7 +6291,7 @@
"iconv-lite": "0.4.24",
"on-finished": "2.4.1",
"qs": "6.11.0",
- "raw-body": "2.5.1",
+ "raw-body": "2.5.2",
"type-is": "~1.6.18",
"unpipe": "1.0.0"
},
@@ -7055,9 +7055,9 @@
"integrity": "sha512-Kvp459HrV2FEJ1CAsi1Ku+MY3kasH19TFykTz2xWmMeq6bk2NU3XXvfJ+Q61m0xktWwt+1HSYf3JZsTms3aRJg=="
},
"node_modules/cookie": {
- "version": "0.5.0",
- "resolved": "https://registry.npmjs.org/cookie/-/cookie-0.5.0.tgz",
- "integrity": "sha512-YZ3GUyn/o8gfKJlnlX7g7xq4gyO6OSuhGPKaaGssGB2qgDUS0gPgtTvoyZLTt9Ab6dC4hfc9dV5arkvc/OCmrw==",
+ "version": "0.6.0",
+ "resolved": "https://registry.npmjs.org/cookie/-/cookie-0.6.0.tgz",
+ "integrity": "sha512-U71cyTamuh1CRNCfpGY6to28lxvNwPG4Guz/EVjgf3Jmzv0vlDp1atT9eS5dDjMYHucpHbWns6Lwf3BKz6svdw==",
"engines": {
"node": ">= 0.6"
}
@@ -7948,16 +7948,16 @@
}
},
"node_modules/express": {
- "version": "4.18.2",
- "resolved": "https://registry.npmjs.org/express/-/express-4.18.2.tgz",
- "integrity": "sha512-5/PsL6iGPdfQ/lKM1UuielYgv3BUoJfz1aUwU9vHZ+J7gyvwdQXFEBIEIaxeGf0GIcreATNyBExtalisDbuMqQ==",
+ "version": "4.19.2",
+ "resolved": "https://registry.npmjs.org/express/-/express-4.19.2.tgz",
+ "integrity": "sha512-5T6nhjsT+EOMzuck8JjBHARTHfMht0POzlA60WV2pMD3gyXw2LZnZ+ueGdNxG+0calOJcWKbpFcuzLZ91YWq9Q==",
"dependencies": {
"accepts": "~1.3.8",
"array-flatten": "1.1.1",
- "body-parser": "1.20.1",
+ "body-parser": "1.20.2",
"content-disposition": "0.5.4",
"content-type": "~1.0.4",
- "cookie": "0.5.0",
+ "cookie": "0.6.0",
"cookie-signature": "1.0.6",
"debug": "2.6.9",
"depd": "2.0.0",
@@ -8200,9 +8200,9 @@
}
},
"node_modules/follow-redirects": {
- "version": "1.15.5",
- "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.5.tgz",
- "integrity": "sha512-vSFWUON1B+yAw1VN4xMfxgn5fTUiaOzAJCKBwIIgT/+7CuGy9+r+5gITvP62j3RmaD5Ph65UaERdOSRGUzZtgw==",
+ "version": "1.15.6",
+ "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.6.tgz",
+ "integrity": "sha512-wWN62YITEaOpSK584EZXJafH1AGpO8RVgElfkuXbTOrPX4fIfOyEpW/CsiNd8JdYrAoOvafRTOEnvsO++qCqFA==",
"funding": [
{
"type": "individual",
@@ -10211,9 +10211,9 @@
}
},
"node_modules/katex": {
- "version": "0.16.9",
- "resolved": "https://registry.npmjs.org/katex/-/katex-0.16.9.tgz",
- "integrity": "sha512-fsSYjWS0EEOwvy81j3vRA8TEAhQhKiqO+FQaKWp0m39qwOzHVBgAUBIXWj1pB+O2W3fIpNa6Y9KSKCVbfPhyAQ==",
+ "version": "0.16.10",
+ "resolved": "https://registry.npmjs.org/katex/-/katex-0.16.10.tgz",
+ "integrity": "sha512-ZiqaC04tp2O5utMsl2TEZTXxa6WSC4yo0fv5ML++D3QZv/vx2Mct0mTlRx3O+uUkjfuAgOkzsCmq5MiUEsDDdA==",
"funding": [
"https://opencollective.com/katex",
"https://github.com/sponsors/katex"
@@ -13496,9 +13496,9 @@
}
},
"node_modules/raw-body": {
- "version": "2.5.1",
- "resolved": "https://registry.npmjs.org/raw-body/-/raw-body-2.5.1.tgz",
- "integrity": "sha512-qqJBtEyVgS0ZmPGdCFPWJ3FreoqvG4MVQln/kCgF7Olq95IbOp0/BWyMwbdtn4VTvkM8Y7khCQ2Xgk/tcrCXig==",
+ "version": "2.5.2",
+ "resolved": "https://registry.npmjs.org/raw-body/-/raw-body-2.5.2.tgz",
+ "integrity": "sha512-8zGqypfENjCIqGhgXToC8aB2r7YrBX+AQAfIPs/Mlk+BtPTztOvTS01NRW/3Eh60J+a48lt8qsCzirQ6loCVfA==",
"dependencies": {
"bytes": "3.1.2",
"http-errors": "2.0.0",
@@ -16035,9 +16035,9 @@
}
},
"node_modules/vite": {
- "version": "4.5.2",
- "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.2.tgz",
- "integrity": "sha512-tBCZBNSBbHQkaGyhGCDUGqeo2ph8Fstyp6FMSvTtsXeZSPpSMGlviAOav2hxVTqFcx8Hj/twtWKsMJXNY0xI8w==",
+ "version": "4.5.3",
+ "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.3.tgz",
+ "integrity": "sha512-kQL23kMeX92v3ph7IauVkXkikdDRsYMGTVl5KY2E9OY4ONLvkHf04MDTbnfo6NKxZiDLWzVpP5oTa8hQD8U3dg==",
"dependencies": {
"esbuild": "^0.18.10",
"postcss": "^8.4.27",
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 92ef133..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": "f193a3d02bbe96cafc462fcb54d5ca73374fd553",
+ "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