steps towards chinese nng

.i18n/config.json

@@ -1,4 +1,5 @@
 {
   "sourceLang": "en",
-  "translationContactEmail": ""
+  "translationContactEmail": "",
+  "useJson": true
 }

.i18n/Game-zh_CN.po → .i18n/zh/Game.po

@@ -6,7 +6,7 @@ msgstr ""
 "Report-Msgid-Bugs-To: \n"
 "POT-Creation-Date: Mon Mar 18 16:33:40 2024\n"
 "PO-Revision-Date: \n"
-"Last-Translator: \n"
+"Last-Translator: @JiechengZhao \n"
 "Language-Team: none\n"
 "Language: zh_CN\n"
 "MIME-Version: 1.0\n"
@@ -639,7 +639,7 @@ msgid ""
 "## Details\n"
 "\n"
 "A mathematician sometimes thinks of `add_zero`\n"
-"as \"one thing\", namely a proof of $\forall n ∈ ℕ, n + 0 = n$.\n"
+"as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.\n"
 "This is just another way of saying that it's a function which\n"
 "can eat any number n and will return a proof that `n + 0 = n`."
 msgstr ""
@@ -2493,7 +2493,7 @@ msgid ""
 "You can think of `succ_inj` itself as a proof; it is the proof\n"
 "that `succ` is an injective function. In other words,\n"
 "`succ_inj` is a proof of\n"
-"$\forall a, b \\in  \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
+"$\\forall a, b \\in  \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n"
 "\n"
 "`succ_inj` was postulated as an axiom by Peano, but\n"
 "in Lean it can be proved using `pred`, a mathematically\n"

Game.lean

@@ -17,6 +17,7 @@ import Game.Levels.AdvMultiplication
 --import Game.Levels.StrongInduction
 --import Game.Levels.Hard
 import Game.Levels.Algorithm
+import I18n
 
 -- Here's what we'll put on the title screen
 Title "Natural Number Game"
@@ -101,7 +102,7 @@ Alternatively, if you experience issues / bugs you can also open github issues:
 -- Dependency Implication → Power -- `Power` uses `≠` which is introduced in `Implication`
 
 /-! Information to be displayed on the servers landing page. -/
-Languages "English"
+Languages "en" "zh"
 CaptionShort "The classical introduction game for Lean."
 CaptionLong "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,
 learning the basics about theorem proving in Lean.

lake-manifest.json

@@ -13,19 +13,19 @@
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "rev": "2c5ce050296621fda7f938b270a18d00672d556b",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
    "subDir": "server",
-   "rev": "68f84a3426684914f834342854bf4963ba2d8d57",
+   "rev": "1a54edffd49bc49f699de74c868656d1914f00c0",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "dev",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",

lakefile.lean

@@ -11,7 +11,8 @@ def LocalGameServer : Dependency := {
 
 def RemoteGameServer : Dependency := {
   name := `GameServer
-  src := Source.git "https://github.com/leanprover-community/lean4game.git" leanVersion "server"
+  -- TODO: change back to stable version
+  src := Source.git "https://github.com/leanprover-community/lean4game.git" "dev" "server" -- leanVersion "server"
 }
 
 /- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/