From 97519537b7fdc85314d8e342e5349c5108bcf3cd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 10 Apr 2024 16:23:24 +0200 Subject: [PATCH] bump to v4.7.0 --- .gitignore | 1 + .i18n/de/Game.json | 23 ++++++++ .i18n/de/Game.po | 114 ++++++++++++++++++++++++++++++++++++++++ .i18n/{ => en}/Game.pot | 32 ++++++----- lake-manifest.json | 30 ++++++++--- lean-toolchain | 2 +- 6 files changed, 182 insertions(+), 20 deletions(-) create mode 100644 .i18n/de/Game.json create mode 100644 .i18n/de/Game.po rename .i18n/{ => en}/Game.pot (68%) diff --git a/.gitignore b/.gitignore index 32f4763..e8593bf 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ build/ lake-packages/ .lake/ **/.DS_Store +.i18n/**/*.mo diff --git a/.i18n/de/Game.json b/.i18n/de/Game.json new file mode 100644 index 0000000..458948e --- /dev/null +++ b/.i18n/de/Game.json @@ -0,0 +1,23 @@ +{"level completed! 🎉": "Level gelöst! 🎉", + "level completed with warnings… 🎭": "Level mit Warnungen beendet… 🎭", + "intermediate goal solved! 🎉": "Zwischenziel gelöst! 🎉", + "You should use this game as a template for your own game and add your own levels.": + "Dieses Spiel sollte als Grundgerüst für eigene Spiele verwendet und eigene Levels hinzugefügt werden.", + "You should use `«{h}»` now.": "Jetzt sollte `«{h}»` verwendet werden.", + "You should use `«{g}»` now.": "Jetzt sollte `«{g}»` verwendet werden.", + "You can either start using `«{h}»` or `«{g}»`.": + "Anfangen kann man mit der Benützung von `«{h}»` oder `«{g}»`.", + "This text is shown as first message when the level is played.\nYou can insert hints in the proof below. They will appear in this side panel\ndepending on the proof a user provides.": + "Dieser Text erscheint als erste Nachricht beim Spielen des Levels.\n\"Hints\" können in den folgenden Beweis eingefügt werden. Diese erscheinen hier in diesem Side-Panel,\nabhängig von dem Beweisstand des Spielers.", + "This text appears on the starting page where one selects the world/level to play.\nYou can use markdown.": + "Dieser Text erscheint auf der Startseite, wo man Welten/Levels zum spielen auswählt.\nMan kann Markdown verwenden.", + "This last message appears if the level is solved.": + "Diese letzte Nachricht erscheint beim erfolgreichen lösen eines Levels.", + "This introduction is shown before one enters level 1 of the demo world. Use markdown.": + "Diese Einführung wird gezeigt, bevor man Level 1 der Beispielwelt öffnet. Man kann Markdown verwenden.", + "Here you can put additional information about the game. It is accessible\nfrom the starting through the drop-down menu.\n\nFor example: Game version, Credits, Link to Github and Zulip, etc.\n\nUse markdown.": + "Hier können zusätzliche Inforamtionen über das Spiel hingeschrieben werden. Man erreicht diese\nvon der Startseite via Dropdown-Menü.\n\nZum Beispiel: Spielversion, Credits, Link auf Github und Zulip, etc.\n\nMan kann Markdown verwenden.", + "Hello World Game": "Hallo-Welt-Spiel", + "Hello World": "Hallo Welt", + "Game Template": "Spiel-Grundgerüst", + "Demo World": "Beispielwelt"} \ No newline at end of file diff --git a/.i18n/de/Game.po b/.i18n/de/Game.po new file mode 100644 index 0000000..07b1e91 --- /dev/null +++ b/.i18n/de/Game.po @@ -0,0 +1,114 @@ +msgid "" +msgstr "" +"Project-Id-Version: Game v4.7.0\n" +"Report-Msgid-Bugs-To: \n" +"POT-Creation-Date: Wed Apr 10 15:31:40 2024\n" +"PO-Revision-Date: \n" +"Last-Translator: \n" +"Language-Team: none\n" +"Language: de\n" +"MIME-Version: 1.0\n" +"Content-Type: text/plain; charset=UTF-8\n" +"Content-Transfer-Encoding: 8bit\n" +"Plural-Forms: nplurals=2; plural=(n != 1);\n" +"X-Generator: Poedit 3.0.1\n" + +#: GameServer.RpcHandlers +msgid "level completed! 🎉" +msgstr "Level gelöst! 🎉" + +#: GameServer.RpcHandlers +msgid "level completed with warnings… 🎭" +msgstr "Level mit Warnungen beendet… 🎭" + +#: GameServer.RpcHandlers +msgid "intermediate goal solved! 🎉" +msgstr "Zwischenziel gelöst! 🎉" + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "Hello World" +msgstr "Hallo Welt" + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "" +"This text is shown as first message when the level is played.\n" +"You can insert hints in the proof below. They will appear in this side " +"panel\n" +"depending on the proof a user provides." +msgstr "" +"Dieser Text erscheint als erste Nachricht beim Spielen des Levels.\n" +"\"Hints\" können in den folgenden Beweis eingefügt werden. Diese erscheinen " +"hier in diesem Side-Panel,\n" +"abhängig von dem Beweisstand des Spielers." + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "You can either start using `«{h}»` or `«{g}»`." +msgstr "Anfangen kann man mit der Benützung von `«{h}»` oder `«{g}»`." + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "You should use `«{h}»` now." +msgstr "Jetzt sollte `«{h}»` verwendet werden." + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "You should use `«{g}»` now." +msgstr "Jetzt sollte `«{g}»` verwendet werden." + +#: Game.Levels.DemoWorld.L01_HelloWorld +msgid "This last message appears if the level is solved." +msgstr "" +"Diese letzte Nachricht erscheint beim erfolgreichen lösen eines Levels." + +#: Game.Levels.DemoWorld +msgid "Demo World" +msgstr "Beispielwelt" + +#: Game.Levels.DemoWorld +msgid "" +"This introduction is shown before one enters level 1 of the demo world. Use " +"markdown." +msgstr "" +"Diese Einführung wird gezeigt, bevor man Level 1 der Beispielwelt öffnet. " +"Man kann Markdown verwenden." + +#: Game +msgid "Hello World Game" +msgstr "Hallo-Welt-Spiel" + +#: Game +msgid "" +"This text appears on the starting page where one selects the world/level to " +"play.\n" +"You can use markdown." +msgstr "" +"Dieser Text erscheint auf der Startseite, wo man Welten/Levels zum spielen " +"auswählt.\n" +"Man kann Markdown verwenden." + +#: Game +msgid "" +"Here you can put additional information about the game. It is accessible\n" +"from the starting through the drop-down menu.\n" +"\n" +"For example: Game version, Credits, Link to Github and Zulip, etc.\n" +"\n" +"Use markdown." +msgstr "" +"Hier können zusätzliche Inforamtionen über das Spiel hingeschrieben werden. " +"Man erreicht diese\n" +"von der Startseite via Dropdown-Menü.\n" +"\n" +"Zum Beispiel: Spielversion, Credits, Link auf Github und Zulip, etc.\n" +"\n" +"Man kann Markdown verwenden." + +#: Game +msgid "Game Template" +msgstr "Spiel-Grundgerüst" + +#: Game +msgid "" +"You should use this game as a template for your own game and add your own " +"levels." +msgstr "" +"Dieses Spiel sollte als Grundgerüst für eigene Spiele verwendet und eigene " +"Levels hinzugefügt werden." diff --git a/.i18n/Game.pot b/.i18n/en/Game.pot similarity index 68% rename from .i18n/Game.pot rename to .i18n/en/Game.pot index 83e931b..029b50f 100644 --- a/.i18n/Game.pot +++ b/.i18n/en/Game.pot @@ -1,13 +1,25 @@ msgid "" -msgstr "Project-Id-Version: Game v4.6.0\n" +msgstr "Project-Id-Version: Game v4.7.0\n" "Report-Msgid-Bugs-To: \n" -"POT-Creation-Date: Thu Feb 29 16:58:28 2024\n" +"POT-Creation-Date: Wed Apr 10 15:31:40 2024\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" "Content-Type: text/plain; charset=UTF-8\n" "Content-Transfer-Encoding: 8bit" +#: GameServer.RpcHandlers +msgid "level completed! 🎉" +msgstr "" + +#: GameServer.RpcHandlers +msgid "level completed with warnings… 🎭" +msgstr "" + +#: GameServer.RpcHandlers +msgid "intermediate goal solved! 🎉" +msgstr "" + #: Game.Levels.DemoWorld.L01_HelloWorld msgid "Hello World" msgstr "" @@ -39,9 +51,7 @@ msgid "Demo World" msgstr "" #: Game.Levels.DemoWorld -msgid "\n" -"This introduction is shown before one enters level 1 of the demo world. Use markdown.\n" -"" +msgid "This introduction is shown before one enters level 1 of the demo world. Use markdown." msgstr "" #: Game @@ -49,21 +59,17 @@ msgid "Hello World Game" msgstr "" #: Game -msgid "\n" -"This text appears on the starting page where one selects the world/level to play.\n" -"You can use markdown.\n" -"" +msgid "This text appears on the starting page where one selects the world/level to play.\n" +"You can use markdown." msgstr "" #: Game -msgid "\n" -"Here you can put additional information about the game. It is accessible\n" +msgid "Here you can put additional information about the game. It is accessible\n" "from the starting through the drop-down menu.\n" "\n" "For example: Game version, Credits, Link to Github and Zulip, etc.\n" "\n" -"Use markdown.\n" -"" +"Use markdown." msgstr "" #: Game diff --git a/lake-manifest.json b/lake-manifest.json index 1f99806..1f4e67f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,28 +4,46 @@ [{"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": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/hhu-adam/lean-i18n.git", "type": "git", "subDir": null, - "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5", + "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39", "name": "i18n", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "v4.7.0", + "inherited": true, + "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": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean4game.git", "type": "git", "subDir": "server", - "rev": "68f84a3426684914f834342854bf4963ba2d8d57", + "rev": "66aa8e688ec6d684bc2ad37c7eee46627a0481b2", "name": "GameServer", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "v4.7.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "Game", diff --git a/lean-toolchain b/lean-toolchain index 5026204..9ad3040 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0 +leanprover/lean4:v4.7.0