From d3a55a4dd36be3c47fff450fcc759193393eb33b Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Thu, 28 Mar 2024 10:07:57 +0800 Subject: [PATCH 1/7] add Chinese translation --- client/public/locales/zh/translation.json | 95 +++++++++++++++++++++++ client/src/config.json | 2 +- 2 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 client/public/locales/zh/translation.json diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json new file mode 100644 index 0000000..683c769 --- /dev/null +++ b/client/public/locales/zh/translation.json @@ -0,0 +1,95 @@ +{ + "Tactics": "策略", + "Lean Game Server": "Lean游戏服务器", + "

Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.

<1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp in a level, you can use it henceforth in any level.

The options are:

": "

游戏规则决定是否允许跳过关卡，以及游戏是否允许在证明中使用未解锁的策略和定理。

<1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在另一个关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp，那么你可以在任何关卡中使用它。

选项是：

", + "Game Rules": "游戏规则", + "levels": "关卡", + "tactics": "策略", + "regular": "标准", + "relaxed": "休闲", + "none": "无", + "Rules": "规则", + "Intro": "介绍", + "Game Introduction": "游戏介绍", + "World selection": "世界选择", + "Start": "开始", + "Inventory": "定理清单", + "next level": "下一关", + "Next": "下一步", + "back to world selection": "返回世界选择", + "Leave World": "离开世界", + "previous level": "上一关", + "Previous": "上一步", + "Editor mode is enforced!": "编辑器模式开启！", + "Editor mode": "编辑器模式", + "Typewriter mode": "打字机模式", + "information, Impressum, privacy policy": "信息、版权声明、隐私政策", + "Impressum": "版权声明", + "Preferences": "偏好设置", + "Game Info & Credits": "游戏信息和荣誉", + "Game Info": "游戏信息", + "Clear Progress": "清除进度", + "Erase": "删除", + "Download Progress": "下载进度", + "Download": "下载", + "Load Progress from JSON": "从 JSON 加载进度", + "Upload": "上传", + "Home": "首页", + "back to games selection": "返回游戏选择", + "close inventory": "关闭定理清单面板", + "show inventory": "打开定理清单面板", + "World": "世界", + "Show more help!": "显示更多帮助！", + "Goal": "目标", + "Current Goal": "当前目标", + "Objects": "Objects", + "Assumptions": "假设", + "Further Goals": "Further Goals", + "No Goals": "无目标", + "Loading goal…": "加载目标...", + "Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。", + "Waiting for Lean server to start…": "等待 Lean 服务器启动...", + "Level completed! 🎉": "完成关卡！🎉", + "Level completed with warnings 🎭": "关卡完成（带有警告） 🎭", + "Retry proof from here": "从这里重新试着证明", + "Active Goal": "当前目标", + "Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：", + "Line": "行", + "Character": "字符", + "Loading messages…": "正在加载信息...", + "Execute": "执行", + "Definitions": "定义", + "Theorems": "定理", + "locked": "锁定中", + "disabled": "已禁用", + "new": "新建", + "Not unlocked yet": "尚未解锁", + "Not available in this level": "本关卡不提供", + "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "一个用于<1>Lean （Lean 4）及其数学库<5>mathlib的学习游戏库", + "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "没有加载游戏。使用<1>http://localhost:3000/#/g/local/FOLDER直接从本地文件夹打开游戏。", + "

As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "

由于这个服务器在我们大学的机器上运行Lean，它的容量是有限的。我们当前的估计是大约70个同时进行的游戏。我们希望将来能更好地解决和测试这个限制。

<1>游戏和基础设施的大多数方面仍在开发中。遇到任何问题，请随时提交<1>GitHub Issue！", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.

Featured games on this page are added manually. Please get in contact and we-ll happily add yours.

": "<0>如果您想编写自己的游戏，您应该使用<1>GameSkeleton Github Repo作为模板，并阅读<3>如何创建游戏。<1>您可以直接将游戏加载到服务器上并使用正确的URL进行游戏。上面的<1>说明也解释了如何将游戏加载到服务器的详细步骤。如果您有任何疑问，请您与我们联系。

本页面上的游戏是手动添加的。请与我们联系，我们很乐意添加您的游戏。

", + "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "这个服务器是作为杜塞尔多夫海因里希·海涅大学项目<1>ADAM：预见数学的数字时代的一部分而开发的。", + "Prerequisites": "前置条件", + "Worlds": "世界(Worlds)", + "Levels": "关卡", + "Language": "语言", + "Development notes": "开发信息", + "Adding new games": "添加新游戏", + "Funding": "赞助", + "

Do you want to delete your saved progress irreversibly?

(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)

": "

您是否想要不可逆转地删除您的游戏进度？

（这将删除您的证明和您收集的定理和策略。其他游戏的进度不会被删除。）

", + "Delete Progress?": "删除进度？", + "Delete": "删除", + "Download & Delete": "下载和删除", + "Cancel": "取消", + "Layout": "布局", + "Always visible": "始终可见", + "Save my settings (in the browser store)": "保存我的设置（在浏览器商店中）", + "

Select a JSON file with the saved game progress to load your progress.

<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "

选择一个包含已保存游戏进度的JSON文件来加载您的进度。

<1><0>警告：这将删除您当前的游戏进度！首先考虑<2>下载您当前的进度！", + "Upload Saved Progress": "上传保存的进度", + "Load selected file": "加载所选文件", + "Mobile": "移动端", + "Auto": "自动", + "Desktop": "桌面端", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.

Featured games on this page are added manually. Please get in contact and we'll happily add yours.

": "<0>如果您想编写自己的游戏，您应该使用<1>GameSkeleton Github Repo作为模板，并阅读<3>如何创建游戏。<1>您可以直接将游戏加载到服务器上并使用正确的URL进行游戏。上面的<1>说明也解释了如何将游戏加载到服务器的详细步骤。如果您有任何疑问，请您与我们联系。

本页面上的游戏是手动添加的。请与我们联系，我们很乐意添加您的游戏。

" +} diff --git a/client/src/config.json b/client/src/config.json index 69e1479..2ff6f2c 100644 --- a/client/src/config.json +++ b/client/src/config.json @@ -21,7 +21,7 @@ { "iso": "zh", "flag": "CN", - "name": "中国话" + "name": "中文" } ] } From 1431ff8b496a0f1563fb46c9124b2e6bcf50d421 Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Thu, 28 Mar 2024 10:21:10 +0800 Subject: [PATCH 2/7] remove the mistyped key --- client/public/locales/zh/translation.json | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index 683c769..c294c00 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -46,9 +46,9 @@ "Assumptions": "假设", "Further Goals": "Further Goals", "No Goals": "无目标", - "Loading goal…": "加载目标...", + "Loading goal…": "加载目标。。。", "Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。", - "Waiting for Lean server to start…": "等待 Lean 服务器启动...", + "Waiting for Lean server to start…": "等待 Lean 服务器启动。。。", "Level completed! 🎉": "完成关卡！🎉", "Level completed with warnings 🎭": "关卡完成（带有警告） 🎭", "Retry proof from here": "从这里重新试着证明", @@ -56,7 +56,7 @@ "Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：", "Line": "行", "Character": "字符", - "Loading messages…": "正在加载信息...", + "Loading messages…": "正在加载信息。。。", "Execute": "执行", "Definitions": "定义", "Theorems": "定理", @@ -68,7 +68,7 @@ "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "一个用于<1>Lean （Lean 4）及其数学库<5>mathlib的学习游戏库", "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "没有加载游戏。使用<1>http://localhost:3000/#/g/local/FOLDER直接从本地文件夹打开游戏。", "

As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "

由于这个服务器在我们大学的机器上运行Lean，它的容量是有限的。我们当前的估计是大约70个同时进行的游戏。我们希望将来能更好地解决和测试这个限制。

<1>游戏和基础设施的大多数方面仍在开发中。遇到任何问题，请随时提交<1>GitHub Issue！", - "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.

Featured games on this page are added manually. Please get in contact and we-ll happily add yours.

": "<0>如果您想编写自己的游戏，您应该使用<1>GameSkeleton Github Repo作为模板，并阅读<3>如何创建游戏。<1>您可以直接将游戏加载到服务器上并使用正确的URL进行游戏。上面的<1>说明也解释了如何将游戏加载到服务器的详细步骤。如果您有任何疑问，请您与我们联系。

本页面上的游戏是手动添加的。请与我们联系，我们很乐意添加您的游戏。

", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.

Featured games on this page are added manually. Please get in contact and we'll happily add yours.

": "<0>如果您想编写自己的游戏，您应该使用<1>GameSkeleton Github Repo作为模板，并阅读<3>如何创建游戏。<1>您可以直接将游戏加载到服务器上并使用正确的URL进行游戏。上面的<1>说明也解释了如何将游戏加载到服务器的详细步骤。如果您有任何疑问，请您与我们联系。

本页面上的游戏是手动添加的。请与我们联系，我们很乐意添加您的游戏。

", "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "这个服务器是作为杜塞尔多夫海因里希·海涅大学项目<1>ADAM：预见数学的数字时代的一部分而开发的。", "Prerequisites": "前置条件", "Worlds": "世界(Worlds)", @@ -90,6 +90,5 @@ "Load selected file": "加载所选文件", "Mobile": "移动端", "Auto": "自动", - "Desktop": "桌面端", - "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.

Featured games on this page are added manually. Please get in contact and we'll happily add yours.

": "<0>如果您想编写自己的游戏，您应该使用<1>GameSkeleton Github Repo作为模板，并阅读<3>如何创建游戏。<1>您可以直接将游戏加载到服务器上并使用正确的URL进行游戏。上面的<1>说明也解释了如何将游戏加载到服务器的详细步骤。如果您有任何疑问，请您与我们联系。

本页面上的游戏是手动添加的。请与我们联系，我们很乐意添加您的游戏。

" + "Desktop": "桌面端" } From 470a184cac47c933b94fe0b84607d596cd9ed45a Mon Sep 17 00:00:00 2001 From: Jiecheng Date: Mon, 1 Apr 2024 07:44:34 +0800 Subject: [PATCH 3/7] some update --- client/public/locales/zh/translation.json | 6 +++--- client/src/components/level.tsx | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index 4b77436..50c9484 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -7,7 +7,7 @@ "tactics": "策略", "regular": "标准", "relaxed": "休闲", - "none": "无", + "none": "自由", "Rules": "规则", "Intro": "介绍", "Game Introduction": "游戏介绍", @@ -15,11 +15,11 @@ "Start": "开始", "Inventory": "定理清单", "next level": "下一关", - "Next": "下一步", + "Next": "下一关", "back to world selection": "返回世界选择", "Leave World": "离开世界", "previous level": "上一关", - "Previous": "上一步", + "Previous": "上一关", "Editor mode is enforced!": "编辑器模式开启！", "Editor mode": "编辑器模式", "Typewriter mode": "打字机模式", diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 260a196..b5933e0 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -466,7 +466,7 @@ function IntroductionPanel({gameInfo}) { {gameInfo.data?.worldSize[worldId] == 0 ? : } From af5426856e9233f43a181c35b214918e43ad327c Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Mon, 1 Apr 2024 12:35:17 +0800 Subject: [PATCH 4/7] Some updates, and fix. --- client/public/locales/zh/translation.json | 2 +- client/src/components/infoview/goals.tsx | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index 50c9484..a2e54bf 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -41,7 +41,7 @@ "Show more help!": "显示更多帮助！", "Goal": "目标", "Current Goal": "当前目标", - "Objects": "Objects", + "Objects": "对象", "Assumptions": "假设", "Further Goals": "Further Goals", "No Goals": "无目标", diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index bbd7f29..41e79bf 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -140,6 +140,7 @@ interface GoalProps { * provided `filter`. */ export const Goal = React.memo((props: GoalProps) => { const { goal, filter, showHints, typewriter } = props + let { t } = useTranslation() // TODO: Apparently `goal` can be `undefined` if (!goal) {return <>} @@ -153,7 +154,7 @@ export const Goal = React.memo((props: GoalProps) => { undefined, [locs, goal.mvarId]) const goalLi =
-
Goal:
+
{t("Goal")}:
@@ -171,10 +172,10 @@ export const Goal = React.memo((props: GoalProps) => { {/* {goal.userName &&
case {goal.userName}
} */} {filter.reverse && goalLi} {! typewriter && objectHyps.length > 0 && -
Objects:
+
{t("Objects")}:
{objectHyps.map((h, i) => )}
} {!typewriter && assumptionHyps.length > 0 && -
Assumptions:
+
{t("Assumptions")}:
{assumptionHyps.map((h, i) => )}
} {!filter.reverse && goalLi} {/* {showHints && hints} */} From d034148bec3a433eac40cf3be2573bc1c2c0299e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 11 Apr 2024 10:30:08 +0200 Subject: [PATCH 5/7] Update README.md --- README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/README.md b/README.md index 2b31007..8d7680f 100644 --- a/README.md +++ b/README.md @@ -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. From c5df85ce665c665679fcb3772b2f481047791be6 Mon Sep 17 00:00:00 2001 From: Hydrogenbear Date: Thu, 11 Apr 2024 19:38:33 +0800 Subject: [PATCH 6/7] Add a missed translation --- client/public/locales/zh/translation.json | 9 +++++---- client/src/components/infoview/main.tsx | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index eceb399..05f5105 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -59,6 +59,7 @@ "Execute": "执行", "Definitions": "定义", "Theorems": "定理", + "Theorem": "定理", "Not unlocked yet": "尚未解锁", "Not available in this level": "本关卡不提供", "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "一个用于<1>Lean （Lean 4）及其数学库<5>mathlib的学习游戏库", @@ -87,8 +88,8 @@ "Mobile": "移动端", "Auto": "自动", "Desktop": "桌面端", - "Level": "", - "Introduction": "", - "Retry": "", - "Failed command": "" + "Level": "关卡", + "Introduction": "介绍", + "Retry": "重试", + "Failed command": "命令失败" } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 1161652..729600b 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -144,7 +144,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
{data?.descrText && - {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})} + {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})} } {data?.descrFormat && showLeanStatement && From 4e7c958348e942bd53381d5b812c3ce206057a32 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 18 Apr 2024 12:24:29 +0200 Subject: [PATCH 7/7] Update client/public/locales/zh/translation.json --- client/public/locales/zh/translation.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index 05f5105..947dc54 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -23,7 +23,7 @@ "Editor mode is enforced!": "编辑器模式开启！", "Editor mode": "编辑器模式", "Typewriter mode": "打字机模式", - "information, Impressum, privacy policy": "信息、版权声明、隐私政策", + "information, Impressum, privacy policy": "信息、版权声明 (Impressum)、隐私政策", "Preferences": "偏好设置", "Game Info & Credits": "游戏信息和荣誉", "Game Info": "游戏信息",