partial bump to v4.8.0: simple fixes

server/GameServer/EnvExtensions.lean

@@ -190,7 +190,7 @@ def getCurLayer [MonadError m] : m Layer := do
 def getCurGameId [Monad m] : m Name := do
   match curGameExt.getState (← getEnv) with
   | some game => return game
-  | none => return defaultGameName
+  | none => return (.mkSimple defaultGameName)
 
 /-- Get the current world -/
 def getCurWorldId [MonadError m] : m Name := do
@@ -468,8 +468,8 @@ def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
 
 def getCurGame [Monad m] : m Game := do
   let some game ← getGame? (← getCurGameId)
-    | let game := {name := defaultGameName}
+    | let game := {name := (.mkSimple defaultGameName)}
-      insertGame defaultGameName game
+      insertGame (.mkSimple defaultGameName) game
       return game
   return game
 

server/GameServer/Helpers/PrettyPrinter.lean

@@ -3,7 +3,7 @@ import Lean.PrettyPrinter.Delaborator.Builtins
 import Lean.PrettyPrinter
 import Lean
 
-import Std.Tactic.OpenPrivate
+import Batteries.Tactic.OpenPrivate
 
 namespace GameServer
 

server/GameServer/ImportModules.lean

@@ -1,5 +1,5 @@
 import Lean.Environment
-import Std.Tactic.OpenPrivate
+import Batteries.Tactic.OpenPrivate
 import Lean.Data.Lsp.Communication
 
 open Lean

server/GameServer/Inventory.lean

@@ -124,7 +124,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
     let allowed := GameServer.ALLOWED_KEYWORDS
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      return {acc with tactics := acc.tactics.insert val}
+      return {acc with tactics := acc.tactics.insert (.mkSimple val)}
     else
       return acc
   | .ident _info _rawVal val _preresolved =>

server/GameServer/RpcHandlers.lean

@@ -17,7 +17,7 @@ def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String)
   let fileParts := fileName.splitOn "/"
   if fileParts.length == 3 then
     if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
-      return some {game, world := fileParts[1]!, level := level}
+      return some {game := .mkSimple game, world := .mkSimple fileParts[1]!, level := level}
   return none
 
 def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
@@ -123,7 +123,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
           let mut hintFVarsNames : Array Expr := #[]
           for fvar in hintFVars do
             let name₁ ← fvar.fvarId!.getUserName
-            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨.mkSimple s!"«\{{name₁}}»"⟩
 
           let lctx := (← goal.getDecl).lctx -- the player's local context
           if let some bij ← matchDecls hintFVars lctx.getFVars

server/GameServer/Utils.lean

@@ -35,7 +35,7 @@ elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)?
     | .ofNat val => s!"Nat := {repr val}"
     | .ofInt val => s!"Int := {repr val}"
     | .ofSyntax val => s!"Syntax := {repr val}"
-    if let some val := opts.find name then
+    if let some val := opts.find (.mkSimple name) then
       msg1 := s!"{msg1}  (currently: {val})"
     msg := match verbose with
     | some opt =>

server/lake-manifest.json

@@ -1,13 +1,13 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4.git",
+ [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
-   "name": "std",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -22,20 +22,20 @@
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
+   "rev": "5158ce6720d88fa1f53fdb86aea8d515af69571c",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
+   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "GameServer",
  "lakeDir": ".lake"}

server/lakefile.lean

@@ -6,7 +6,7 @@ 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 std from git "https://github.com/leanprover/std4.git" @ leanVersion
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ leanVersion
 require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
 
 require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
@@ -28,4 +28,4 @@ post_update pkg do
   let rootPkg ← getRootPackage
   if rootPkg.name = pkg.name then
     return -- do not run in GameServer itself
-  discard <| runBuild gameserver.build >>= (·.await)
+  discard <| runBuild gameserver.fetch

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0