From ea680516621f4f385a597a7e3ed9353f8e3b52eb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 27 Jun 2026 14:49:52 +0200 Subject: [PATCH] bump lean --- README.md | 6 ++++-- doc/development.md | 10 ++++++++++ server/GameServer/Hints.lean | 2 +- server/GameServer/RpcHandlers.lean | 7 ++++++- server/GameServer/Tactic/Hint.lean | 2 +- server/lake-manifest.json | 10 +++++----- server/lakefile.lean | 7 ++----- server/lean-toolchain | 2 +- 8 files changed, 30 insertions(+), 16 deletions(-) create mode 100644 doc/development.md diff --git a/README.md b/README.md index cee878f9..55521851 100644 --- a/README.md +++ b/README.md @@ -37,11 +37,13 @@ The documentation is very much work in progress but the links below should be up Contributions to `lean4game` are always welcome! +Check out the [Development Instructions](./doc/development.md) + ### Translation -We welcome translations of the game interface and of the various games hosted on the [Lean Game Server](https://adam.math.hhu.de) into different languages! +We welcome translations of the game interface and of the various games hosted on the [Lean Game Server](https://adam.math.hhu.de) into different languages! -* For translating the *interface*, please refer to [these instructions](doc/translation-interface.md). +* For translating the *interface*, please refer to [these instructions](doc/translation-interface.md). * For translating *individual games*, please contact the maintainers (see [table below](#contact)) and consult any game specific translation guidelines. Our [generic guidlines](doc/translation-guide-for-game-translators.md) may give a rough indication of the steps involved. * We also have some [guidelines for game maintainers](doc/translation-guide-for-game-maintainers.md) regarding translations. diff --git a/doc/development.md b/doc/development.md new file mode 100644 index 00000000..f102c0c4 --- /dev/null +++ b/doc/development.md @@ -0,0 +1,10 @@ +# Development + +## Updating Lean version + +1. make sure `lean-i18n` has been updated +1. edit `server/lean-toolchain` to contain the desired version: `leanprover/lean4:v4.31.0` +2. edit all `require` statements in `server/lakefile.lean` to contain the toolchain (e.g. `"v4.31.0"`) instead of `"main"` +3. call `lake update --keep-toolchain` +4. undo the changes in `server/lakefile.lean` +5. `npm run build:server` diff --git a/server/GameServer/Hints.lean b/server/GameServer/Hints.lean index 30af76e6..8f12937e 100644 --- a/server/GameServer/Hints.lean +++ b/server/GameServer/Hints.lean @@ -32,7 +32,7 @@ instance : Repr GoalHintEntry := { TODO: explain better. -/ unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) := evalExpr (Array Expr → MessageData) - (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) + (.forallE default (mkApp (mkConst ``Array [Level.zero]) (mkConst ``Expr)) (mkConst ``MessageData) .default) @[implemented_by evalHintMessageUnsafe] diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index ac4c4185..2697ef17 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -213,7 +213,12 @@ def getProofState (p : ProofStateParams) : RequestM (RequestTask (Option ProofSt bindTaskCostly doc.cmdSnaps.waitAll fun (snaps, _) => do mapTaskCostly doc.reporter fun () => do let mut steps : Array <| InteractiveGoalsWithHints := #[] - let mut diag : Array InteractiveDiagnostic ← doc.diagnosticsRef.get + + let mut diag : Array InteractiveDiagnostic ← doc.diagnosticsMutex.atomically do + let ds ← get + let stickyDiags ← ds.stickyDiagsRef.get + let diags := ds.diags + return stickyDiags ++ diags |>.toArray -- Level is completed if there are no errors or warnings let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) diff --git a/server/GameServer/Tactic/Hint.lean b/server/GameServer/Tactic/Hint.lean index 96365540..b13535a4 100644 --- a/server/GameServer/Tactic/Hint.lean +++ b/server/GameServer/Tactic/Hint.lean @@ -42,7 +42,7 @@ elab (name := Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => d -- want the text to possibly contain quotation of the local variables which might have been -- named differently by the player. let varsName := `vars - let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do + let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [Level.zero]) (mkConst ``Expr)) fun vars => do let mut text ← `(m! $msg) let goalDecl ← goal.getDecl let decls := goalDecl.lctx.decls.toArray.filterMap id diff --git a/server/lake-manifest.json b/server/lake-manifest.json index b2dacb32..b907390d 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "hhu-adam", - "rev": "084ba4a951815d4757eb13656231a9b405e73bcc", + "rev": "1a99b00a940624c0a6c3009b756fb922acf0fe78", "name": "i18n", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4ee56e687ce2b9b51b097bfa65947a499da0c453", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": false, + "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/server/lakefile.lean b/server/lakefile.lean index be4358e2..2946a5f8 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -3,11 +3,8 @@ open Lake DSL package GameServer --- Using this assumes that each dependency has a tag of the form `v4.X.0`. -def leanVersion : String := s!"v{Lean.versionString}" - -require "leanprover-community" / batteries @ git "main" -require "hhu-adam" / i18n @ git "main" +require "leanprover-community" / batteries @ git "v4.31.0" +require "hhu-adam" / i18n @ git "v4.31.0" -- dev dependency -- require "leanprover-community" / importGraph @ git "main" diff --git a/server/lean-toolchain b/server/lean-toolchain index 635bb953..18640c8b 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0-rc2 \ No newline at end of file +leanprover/lean4:v4.31.0