From 684a1bc72b61e7229e75529b82d8907b7ebf8c40 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 29 Mar 2024 12:16:36 +0100 Subject: [PATCH 01/11] fix initial translation loading on starting page --- client/src/components/landing_page.tsx | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 26ab89b..30fb2d4 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -39,13 +39,16 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { 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 => {}).then(() => {setLoadedTranslation(true)}) + if (typeof data === 'undefined') { return <> } - // Load the namespace of the game - i18next.loadNamespaces(gameId) - return
{t(data.title, { ns: gameId })}
From dd7a2d1bc19795e4c0c5e0a801cad988347e1f42 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 29 Mar 2024 12:23:37 +0100 Subject: [PATCH 02/11] bump lean-i18n --- server/lake-manifest.json | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 1ba5515..92ef133 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -10,10 +10,19 @@ "inputRev": "v4.6.0", "inherited": false, "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": "2c5ce050296621fda7f938b270a18d00672d556b", + "rev": "f193a3d02bbe96cafc462fcb54d5ca73374fd553", "name": "i18n", "manifestFile": "lake-manifest.json", "inputRev": "main", From 39be34e83a3f3f164729ade27a8966fd6e06109a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 29 Mar 2024 12:27:14 +0100 Subject: [PATCH 03/11] improve landing page --- client/src/components/landing_page.tsx | 31 ++++++++++++++++++++------ client/src/components/level.tsx | 4 +++- 2 files changed, 27 insertions(+), 8 deletions(-) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 30fb2d4..5178425 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -43,7 +43,9 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { let [loadedTranslation, setLoadedTranslation] = React.useState(false) // Load the namespace of the game - i18next.loadNamespaces(gameId).catch(err => {}).then(() => {setLoadedTranslation(true)}) + i18next.loadNamespaces(gameId).catch(err => { + console.warn(`translations for ${gameId} do not exist`) + }).then(() => {setLoadedTranslation(true)}) if (typeof data === 'undefined') { return <> @@ -77,10 +79,8 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { {data.languages.map((lang) => { let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang) - if (langOpt) { - return - } else - return <> + return + })} @@ -103,9 +103,26 @@ function LandingPage() { const closePreferencesPopup = () => setPreferencesPopup(false); const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup); - let allTiles = lean4gameConfig.allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) const { t, i18n } = useTranslation() + let allTiles = lean4gameConfig.allGames.map((gameId) => { + + let q = useGetGameInfoQuery({game: `g/${gameId}`}) + + // if (q.isError) { + // if (q.error?.originalStatus === 404) { + // // Handle 404 error + // console.log('File not found'); + // } else { + // // Suppress additional console.error messages + // console.error(q.error); + // } + // } + + return q.data?.tile + }) + + return
- {allTiles.length == 0 ? + {allTiles.filter(x => x != null).length == 0 ?

No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 260a196..b95b38b 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -67,7 +67,9 @@ function Level() { const gameId = React.useContext(GameIdContext) // Load the namespace of the game - i18next.loadNamespaces(gameId) + i18next.loadNamespaces(gameId).catch(err => { + console.warn(`translations for ${gameId} do not exist.`) + }) const gameInfo = useGetGameInfoQuery({game: gameId}) From 5a768c25b72d804154a896f71457e0ed111a01a7 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 29 Mar 2024 12:34:57 +0100 Subject: [PATCH 04/11] mark two more translations --- client/src/components/level.tsx | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index b95b38b..77cb2ca 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -213,6 +213,7 @@ function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableR } function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPopup}) { + let { t } = useTranslation() const codeviewRef = useRef(null) const gameId = React.useContext(GameIdContext) const {worldId, levelId} = useContext(WorldLevelIdContext) @@ -416,7 +417,7 @@ function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPo - + {gameInfo.isLoading ?

: mobile ? From 3124d90cd646ebb039739d18f4a55c5f463a551f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 29 Mar 2024 12:36:39 +0100 Subject: [PATCH 05/11] typo --- client/public/locales/de/translation.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/public/locales/de/translation.json b/client/public/locales/de/translation.json index 05127f4..7eab79f 100644 --- a/client/public/locales/de/translation.json +++ b/client/public/locales/de/translation.json @@ -62,7 +62,7 @@ "locked": "nicht verfügbar", "disabled": "gesperrt", "new": "neu", - "Not unlocked yet": "Not nicht verfügbar", + "Not unlocked yet": "Noch nicht verfügbar", "Not available in this level": "In diesem Level nicht verfügbar", "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean (Lean 4) und dessen mathematische Bibliothek <5>mathlib", "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER um ein Spiel direkt von einem lokalen Ordner zu laden.", From 9b05a27888beb5ee00527385c74d87c79a4a697a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 6 Apr 2024 14:56:19 +0200 Subject: [PATCH 06/11] use translation of level title --- client/src/components/level.tsx | 2 +- server/GameServer/Commands.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 77cb2ca..d459743 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -418,7 +418,7 @@ function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPo pageNumber={pageNumber} setPageNumber={setPageNumber} isLoading={level.isLoading} levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` + - (level?.data?.title && ` : ${level?.data?.title}`)} + (level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)} toggleImpressum={toggleImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup} diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 07a8086..2b8faea 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -42,7 +42,7 @@ elab "Title" t:str : command => do | .Level => modifyCurLevel fun level => pure {level with title := title} | .World => modifyCurWorld fun world => pure {world with title := title} | .Game => modifyCurGame fun game => pure {game with - title := t.getString + title := title tile := {game.tile with title := title}} /-- Define the introduction of the current game/world/level. -/ From a8d3169ebb7f8605bfe958738a72d7e1eb73c001 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 6 Apr 2024 15:25:31 +0200 Subject: [PATCH 07/11] add some translation keys --- client/i18next-scanner.config.cjs | 1 + client/public/locales/de/translation.json | 12 ++++++------ client/public/locales/en/translation.json | 11 ++++++----- client/public/locales/zh/translation.json | 9 +++++---- client/src/components/infoview/main.tsx | 9 +++++---- 5 files changed, 23 insertions(+), 19 deletions(-) diff --git a/client/i18next-scanner.config.cjs b/client/i18next-scanner.config.cjs index 39429b0..e658b99 100644 --- a/client/i18next-scanner.config.cjs +++ b/client/i18next-scanner.config.cjs @@ -78,6 +78,7 @@ module.exports = { ], options: { debug: true, + removeUnusedKeys: true, func: { list: ['i18next.t', 'i18n.t', 't'], extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript! diff --git a/client/public/locales/de/translation.json b/client/public/locales/de/translation.json index 7eab79f..9efb4cd 100644 --- a/client/public/locales/de/translation.json +++ b/client/public/locales/de/translation.json @@ -50,7 +50,6 @@ "Waiting for Lean server to start…": "Warte auf das Starten des Lean-Servers…", "Level completed! 🎉": "Level gelöst! 🎉", "Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭", - "Retry proof from here": "Von hier erneut probieren", "Active Goal": "Aktuelles Goal", "Crashed! Go to editor mode and fix your proof! Last server response:": "", "Line": "Zeile", @@ -59,15 +58,11 @@ "Execute": "Ausführen", "Definitions": "Definitionen", "Theorems": "Theoreme", - "locked": "nicht verfügbar", - "disabled": "gesperrt", - "new": "neu", "Not unlocked yet": "Noch nicht verfügbar", "Not available in this level": "In diesem Level nicht verfügbar", "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean (Lean 4) und dessen mathematische Bibliothek <5>mathlib", "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER um ein Spiel direkt von einem lokalen Ordner zu laden.", "

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!": "", - "<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.

": "", "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.": "", "Prerequisites": "Voraussetzungen", "Worlds": "Welten", @@ -90,5 +85,10 @@ "Mobile": "Mobil", "Auto": "Auto", "Desktop": "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>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.

": "", + "Level": "", + "Introduction": "", + "Retry proof from here": "", + "Retry": "", + "Failed command": "" } diff --git a/client/public/locales/en/translation.json b/client/public/locales/en/translation.json index f1a92b6..68666a6 100644 --- a/client/public/locales/en/translation.json +++ b/client/public/locales/en/translation.json @@ -50,7 +50,6 @@ "Waiting for Lean server to start…": "Waiting for Lean server to start…", "Level completed! 🎉": "Level completed! 🎉", "Level completed with warnings 🎭": "Level completed with warnings 🎭", - "Retry proof from here": "Retry proof from here", "Active Goal": "Active Goal", "Crashed! Go to editor mode and fix your proof! Last server response:": "Crashed! Go to editor mode and fix your proof! Last server response:", "Line": "Line", @@ -59,9 +58,6 @@ "Execute": "Execute", "Definitions": "Definitions", "Theorems": "Theorems", - "locked": "locked", - "disabled": "disabled", - "new": "new", "Not unlocked yet": "Not unlocked yet", "Not available in this level": "Not available in this level", "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib", @@ -89,5 +85,10 @@ "Mobile": "Mobile", "Auto": "Auto", "Desktop": "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>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>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>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.

", + "Level": "Level", + "Introduction": "Introduction", + "Retry proof from here": "Retry proof from here", + "Retry": "Retry", + "Failed command": "Failed command" } diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index b6f6179..fe33128 100644 --- a/client/public/locales/zh/translation.json +++ b/client/public/locales/zh/translation.json @@ -59,9 +59,6 @@ "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": "", @@ -89,5 +86,9 @@ "Load selected file": "加载所选文件", "Mobile": "移动端", "Auto": "自动", - "Desktop": "桌面端" + "Desktop": "桌面端", + "Level": "", + "Introduction": "", + "Retry": "", + "Failed command": "" } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 244f7e9..1161652 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -265,9 +265,10 @@ const goalFilter = { showLetValue: true } -// TODD: Mark for translation! /** The display of a single entered lean command */ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) { + let {t} = useTranslation() + // The first step will always have an empty command if (!proof?.steps[i]?.command) { return <> } @@ -275,13 +276,13 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele // If the last step has errors, we display the command in a different style // indicating that it will be removed on the next try. return
- Failed command: {proof?.steps[i].command} + {t("Failed command")}: {proof?.steps[i].command}
} else { return
{proof?.steps[i].command}
-
} From 7cedfc5038cd5d030c9263f228b56b08407bf6d2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 6 Apr 2024 15:40:06 +0200 Subject: [PATCH 08/11] mark some server messages for translation --- server/GameServer/Commands.lean | 1 + server/GameServer/RpcHandlers.lean | 11 ++++++++--- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 2b8faea..648a253 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -4,6 +4,7 @@ import GameServer.Options import GameServer.SaveData import GameServer.Hints import GameServer.Tactic.LetIntros +import GameServer.RpcHandlers -- only needed to collect the translations of "level completed" msgs import I18n open Lean Meta Elab Command diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index b4b75d7..6ad1578 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -2,6 +2,7 @@ import GameServer.EnvExtensions import GameServer.InteractiveGoal import Std.Data.Array.Init.Basic import GameServer.Hints +import I18n open Lean open Server @@ -171,7 +172,11 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B if goalCount == 0 then if completed then out := out.push { - message := .text "level completed! 🎉" + -- TODO: marking these with `t!` has the implication that every game + -- needs to translate these messages again, + -- but cannot think of another option + -- that would not involve manually adding them somewhere in the translation files. + message := .text t!"level completed! 🎉" range := { start := pos «end» := pos @@ -179,7 +184,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B severity? := Lsp.DiagnosticSeverity.information } else if completedWithWarnings then out := out.push { - message := .text "level completed with warnings… 🎭" + message := .text t!"level completed with warnings… 🎭" range := { start := pos «end» := pos @@ -192,7 +197,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B -- so showing the message "intermediate goal solved" would be confusing. if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then out := out.push { - message := .text "intermediate goal solved! 🎉" + message := .text t!"intermediate goal solved! 🎉" range := { start := pos «end» := pos From ce71bc81c648aedb05a824daf56d5b936329b5d0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 8 Apr 2024 12:23:07 +0200 Subject: [PATCH 09/11] remove logInfo for Branch finishing proof --- server/GameServer/Commands.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 648a253..55bced3 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -577,7 +577,8 @@ elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do -- Show an info whether the branch proofs all remaining goals. let gs ← Tactic.getUnsolvedGoals if gs.isEmpty then - trace[debug] "This branch finishes the proof." + -- trace[debug] "This branch finishes the proof." + pure () else trace[debug] "This branch leaves open goals." From 74059bd5af47782a97b9f5427879a8092254b5eb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 8 Apr 2024 23:20:21 +0200 Subject: [PATCH 10/11] fix typo --- doc/writing_exercises.md | 10 +++++----- server/GameServer/Commands.lean | 18 +++++++++--------- server/GameServer/EnvExtensions.lean | 2 +- server/GameServer/FileWorker.lean | 2 +- server/test/test_statement.lean | 2 +- 5 files changed, 17 insertions(+), 17 deletions(-) diff --git a/doc/writing_exercises.md b/doc/writing_exercises.md index efc9d9e..8d8483e 100644 --- a/doc/writing_exercises.md +++ b/doc/writing_exercises.md @@ -26,23 +26,23 @@ f: ℤ → ℤ := fun x => 2 * x ⊢ 0 < f a ``` -## "Preample" & non-`Prop`-valued exercises +## "Preamble" & non-`Prop`-valued exercises -You can use the following syntax with `(preample := tac)` where `tac` is a tactic sequence. +You can use the following syntax with `(preamble := tac)` where `tac` is a tactic sequence. ``` -Statement my_statement (preample := dsimp) (a : ℤ) (h : 0 < a) : +Statement my_statement (preamble := dsimp) (a : ℤ) (h : 0 < a) : 0 < f a := by sorry ``` This tactic sequence will be executed before the exercise is handed to the player. -For example, if your exercise is to construct a structure, you could use `preample` to fill +For example, if your exercise is to construct a structure, you could use `preamble` to fill all data fields correctly, leaving all `Prop`-valued fields of the structure as separate goals for the player to proof. -Note: `(preample := tac)` always has to be written between the optional name and the first +Note: `(preamble := tac)` always has to be written between the optional name and the first hypothesis. Nevertheless, you can use all hypotheses in the tactic sequence, because it is only evaluated at the beginning of the proof. diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 55bced3..76544f9 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -345,7 +345,7 @@ elab "LemmaTab" category:str : command => do /-! # Exercise Statement -/ -/-- You can write `Statement add_comm (preample := simp) .... := by` which +/-- You can write `Statement add_comm (preamble := simp) .... := by` which will automatically execute the given tactic sequence before the exercise is handed to the player. @@ -361,18 +361,18 @@ For example in "Show that all matrices with first column zero form a submodule", you could provide the set of all these matrices as `carrier` and the player will receive all the `Prop`-valued fields as goals. -/ -syntax preampleArg := atomic(" (preample := " withoutPosition(tacticSeq) ")") +syntax preambleArg := atomic(" (preamble := " withoutPosition(tacticSeq) ")") /-- Define the statement of the current level. -/ elab doc:docComment ? attrs:Parser.Term.attributes ? - "Statement" statementName:ident ? preample:preampleArg ? sig:declSig val:declVal : command => do + "Statement" statementName:ident ? preamble:preambleArg ? sig:declSig val:declVal : command => do let lvlIdx ← getCurLevelIdx -- add an optional tactic sequence that the engine executes before the game starts - let preampleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preample with + let preambleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preamble with | none => `(Parser.Tactic.tacticSeq|skip) | some x => match x with - | `(preampleArg| (preample := $tac)) => pure tac + | `(preambleArg| (preamble := $tac)) => pure tac | _ => `(Parser.Tactic.tacticSeq|skip) let docContent ← parseDocComment doc @@ -414,17 +414,17 @@ elab doc:docComment ? attrs:Parser.Term.attributes ? -- in that case. logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++ m!"statement will be available in later levels:\n\n{origType}") - let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)}) + let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) elabCommand thmStatement -- Check that statement has a docs entry. checkInventoryDoc .Lemma name (name := fullName) (template := docContent) else - let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)}) + let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) elabCommand thmStatement -- Check that statement has a docs entry. checkInventoryDoc .Lemma name (name := fullName) (template := docContent) | none => - let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)}) + let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)}) elabCommand thmStatement let msgs := (← get).messages @@ -499,7 +499,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ? modifyCurLevel fun level => pure { level with module := env.header.mainModule goal := sig, - preample := preampleSeq + preamble := preambleSeq scope := scope, descrText := docContent statementName := match statementName with diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 3229fdc..20be5b3 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -266,7 +266,7 @@ structure GameLevel where /-- The image for this level. -/ image : String := default /-- A sequence of tactics the game automatically executes before the first step. -/ - preample : TSyntax `Lean.Parser.Tactic.tacticSeq := default + preamble : TSyntax `Lean.Parser.Tactic.tacticSeq := default deriving Inhabited, Repr /-- Json-encodable version of `GameLevel` diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 0a012f3..e05915b 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -263,7 +263,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets -- This makes the experience for the user much nicer and allows for local -- definitions in the exercise. let cmdStx ← `(command| - theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preample⟩); $(⟨tacticStx⟩)} ) + theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx⟩)} ) Elab.Command.elabCommandTopLevel cmdStx) cmdCtx cmdStateRef let postNew := (← tacticCacheNew.get).post diff --git a/server/test/test_statement.lean b/server/test/test_statement.lean index f602182..196d1b7 100644 --- a/server/test/test_statement.lean +++ b/server/test/test_statement.lean @@ -81,5 +81,5 @@ example (n m : Nat) : (m + n) + x = m + (n + x) := by #check My.add_assoc -Statement My.add_comm (preample := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by +Statement My.add_comm (preamble := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by rw [Nat.add_comm] From d456621875b24f379c3a836026b6302721aa3d99 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 9 Apr 2024 09:47:05 +0200 Subject: [PATCH 11/11] apply suggestions from PR #206 manually --- client/public/locales/zh/translation.json | 8 ++++---- client/src/components/infoview/goals.tsx | 7 ++++--- client/src/components/level.tsx | 2 +- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/client/public/locales/zh/translation.json b/client/public/locales/zh/translation.json index fe33128..296c575 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": "打字机模式", @@ -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} */} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index d459743..8d06b9e 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -469,7 +469,7 @@ function IntroductionPanel({gameInfo}) { {gameInfo.data?.worldSize[worldId] == 0 ? : }