phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'upstream/dev' into cn-i18n

Browse Source
This commit is contained in:
Hydrogenbear
2024-04-10 08:30:36 +08:00
parent af5426856e d456621875
commit ded9c38170
14 changed files with 101 additions and 56 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/i18next-scanner.config.cjs
+1
View File
@@ -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!
client/public/locales/de/translation.json
+7 -7
View File
@@ -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": "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</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt von einem lokalen Ordner zu laden.",
"<p>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.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we-ll happily add yours.</p>": "",
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> 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</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": ""
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
"Level": "",
"Introduction": "",
"Retry proof from here": "",
"Retry": "",
"Failed command": ""
}
client/public/locales/en/translation.json
+6 -5
View File
@@ -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</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>",
@@ -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</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>"
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>",
"Level": "Level",
"Introduction": "Introduction",
"Retry proof from here": "Retry proof from here",
"Retry": "Retry",
"Failed command": "Failed command"
}
client/public/locales/zh/translation.json
+5 -4
View File
@@ -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</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "一个用于<1>Lean</1> <i>（Lean 4）</i>及其数学库<5>mathlib</5>的学习游戏库",
@@ -89,5 +86,9 @@
"Load selected file": "加载所选文件",
"Mobile": "移动端",
"Auto": "自动",
"Desktop": "桌面端"
"Desktop": "桌面端",
"Level": "",
"Introduction": "",
"Retry": "",
"Failed command": ""
}
client/src/components/infoview/main.tsx
+5 -4
View File
@@ -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 <div className="failed-command">
<i>Failed command</i>: {proof?.steps[i].command}
<i>{t("Failed command")}</i>: {proof?.steps[i].command}
</div>
} else {
return <div className="command">
<div className="command-text">{proof?.steps[i].command}</div>
<Button to="" className="undo-button btn btn-inverted" title={"Retry proof from here"} onClick={deleteProof}>
<FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{"Retry"}
<Button to="" className="undo-button btn btn-inverted" title={t("Retry proof from here")} onClick={deleteProof}>
<FontAwesomeIcon icon={faDeleteLeft} />&nbsp;{t("Retry")}
</Button>
</div>
}
client/src/components/landing_page.tsx
+29 -9
View File
@@ -39,13 +39,18 @@ 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 => {
console.warn(`translations for ${gameId} do not exist`)
}).then(() => {setLoadedTranslation(true)})
if (typeof data === 'undefined') {
return <></>
}
// Load the namespace of the game
i18next.loadNamespaces(gameId)
return <div className="game" onClick={routeChange}>
<div className="wrapper">
<div className="title">{t(data.title, { ns: gameId })}</div>
@@ -74,10 +79,8 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
<td>
{data.languages.map((lang) => {
let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang)
if (langOpt) {
return <ReactCountryFlag title={langOpt.name} countryCode={langOpt.flag} className="emojiFlag"/>
} else
return <></>
return <ReactCountryFlag key={`flag-${lang}`} title={langOpt?.name} countryCode={langOpt?.flag} className="emojiFlag"/>
})}
</td>
</tr>
@@ -100,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 <div className="landing-page">
<header style={{backgroundImage: `url(${bgImage})`}}>
<nav className="landing-page-nav">
@@ -125,7 +145,7 @@ function LandingPage() {
</div>
</header>
<div className="game-list">
{allTiles.length == 0 ?
{allTiles.filter(x => x != null).length == 0 ?
<p>
<Trans>
No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
client/src/components/level.tsx
+9 -4
View File
@@ -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})
@@ -211,6 +213,7 @@ function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableR
}
function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPopup}) {
let { t } = useTranslation()
const codeviewRef = useRef<HTMLDivElement>(null)
const gameId = React.useContext(GameIdContext)
const {worldId, levelId} = useContext(WorldLevelIdContext)
@@ -414,8 +417,8 @@ function PlayableLevel({impressum, setImpressum, toggleInfo, togglePreferencesPo
<LevelAppBar
pageNumber={pageNumber} setPageNumber={setPageNumber}
isLoading={level.isLoading}
levelTitle={`${mobile ? '' : 'Level '}${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
(level?.data?.title && ` : ${level?.data?.title}`)}
levelTitle={(mobile ? "" : t("Level")) + ` ${levelId} / ${gameInfo.data?.worldSize[worldId]}` +
(level?.data?.title && ` : ${t(level?.data?.title, {ns: gameId})}`)}
toggleImpressum={toggleImpressum}
toggleInfo={toggleInfo}
togglePreferencesPopup={togglePreferencesPopup}
@@ -477,6 +480,8 @@ export default Level
/** The site with the introduction text of a world */
function Introduction({impressum, setImpressum, toggleInfo, togglePreferencesPopup}) {
let { t } = useTranslation()
const gameId = React.useContext(GameIdContext)
const {mobile} = useContext(PreferencesContext)
@@ -494,7 +499,7 @@ function Introduction({impressum, setImpressum, toggleInfo, togglePreferencesPop
}
return <>
<LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Introduction" toggleImpressum={toggleImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
<LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
{gameInfo.isLoading ?
<div className="app-content loading"><CircularProgress /></div>
: mobile ?
doc/writing_exercises.md
+5 -5
View File
@@ -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.
server/GameServer/Commands.lean
+13 -11
View File
@@ -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
@@ -42,7 +43,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. -/
@@ -344,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.
@@ -360,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
@@ -413,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
@@ -498,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
@@ -576,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."
server/GameServer/EnvExtensions.lean
+1 -1
View File
@@ -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`
server/GameServer/FileWorker.lean
+1 -1
View File
@@ -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
server/GameServer/RpcHandlers.lean
+8 -3
View File
@@ -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
server/lake-manifest.json
+10 -1
View File
@@ -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",
server/test/test_statement.lean
+1 -1
View File
@@ -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]