chore: bump to Lean v4.31.0 (#534)

Author: joneugster

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.
 

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`

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]

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)

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

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",

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"

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.30.0-rc2
+leanprover/lean4:v4.31.0