Merge branch 'main' of https://github.com/leanprover-community/lean4game into cn-i18n

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.

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 <div className="landing-page">
     <header style={{backgroundImage: `url(${bgImage})`}}>
       <nav className="landing-page-nav">

client/src/config.json

@@ -3,7 +3,6 @@
     "leanprover-community/nng4",
     "hhu-adam/robo",
     "djvelleman/stg4",
-    "miguelmarco/stg4",
     "trequetrum/lean4game-logic"
   ],
 

client/src/css/landing_page.css

@@ -19,7 +19,7 @@ a {
 
 @viewport {
   width: device-width ;
-  zoom: 1.0 ;
+  initial-scale: 1.0 ;
 }
 
 .landing-page {

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<string>) {
         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
     }
   });
 

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)
 

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.

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",

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
 

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",

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
 

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0