support translations of the games

server/GameServer/FileWorker.lean

@@ -331,6 +331,9 @@ structure GameParams where
   diagnostics : GameDiagnostics
 deriving ToJson, FromJson
 
+-- `snap` and `initParams` are unused
+set_option linter.unusedVariables false in
+
 /-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
 def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
     IO Unit := do

server/GameServer/Helpers/PrettyPrinter.lean

@@ -14,9 +14,6 @@ open Lean.Parser Term
 open PrettyPrinter Delaborator SubExpr
 open TSyntax.Compat
 
-
-#check Command.declSig
-
 open private shouldGroupWithNext evalSyntaxConstant from Lean.PrettyPrinter.Delaborator.Builtins
 
 -- def typeSpec := leading_parser " :\\n: " >> termParser

server/GameServer/SaveData.lean

@@ -59,8 +59,8 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
-  -- write PO file for translation
-  I18n.createPOTemplate
+  -- write file for translation
+  I18n.createTemplate
 
 open GameData
 

server/GameServer/Tactic/LetIntros.lean

@@ -52,8 +52,6 @@ If names are provided, it will introduce as many `let` statements as there are n
 syntax (name := letIntros) "let_intros" : tactic
 -- (ppSpace colGt (ident <|> hole))*
 
-#check letIntros
-
 @[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
   match stx with
   | `(tactic| let_intros) => liftMetaTactic fun mvarId => do

server/lake-manifest.json

@@ -13,10 +13,10 @@
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "rev": "59fea5bbc2ea22c2ee77ea6a65b0212ac241a56f",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -8,7 +8,7 @@ package GameServer
 def leanVersion := "v4.6.0" -- TODO
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
-require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
+require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ "main" -- leanVersion
 
 lean_lib GameServer