From 446d0296f0bcb64a195ba595944dbf8e28c93a84 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 7 Jun 2024 02:06:21 +0200 Subject: [PATCH] partial bump to v4.8.0: simple fixes --- server/GameServer/EnvExtensions.lean | 6 +++--- server/GameServer/Helpers/PrettyPrinter.lean | 2 +- server/GameServer/ImportModules.lean | 2 +- server/GameServer/Inventory.lean | 2 +- server/GameServer/RpcHandlers.lean | 4 ++-- server/GameServer/Utils.lean | 2 +- server/lake-manifest.json | 18 +++++++++--------- server/lakefile.lean | 4 ++-- server/lean-toolchain | 2 +- 9 files changed, 21 insertions(+), 21 deletions(-) diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 20be5b3..728bd1e 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/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} - insertGame defaultGameName game + | let game := {name := (.mkSimple defaultGameName)} + insertGame (.mkSimple defaultGameName) game return game return game diff --git a/server/GameServer/Helpers/PrettyPrinter.lean b/server/GameServer/Helpers/PrettyPrinter.lean index 8109565..b8adf49 100644 --- a/server/GameServer/Helpers/PrettyPrinter.lean +++ b/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 diff --git a/server/GameServer/ImportModules.lean b/server/GameServer/ImportModules.lean index 055bed1..e255144 100644 --- a/server/GameServer/ImportModules.lean +++ b/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 diff --git a/server/GameServer/Inventory.lean b/server/GameServer/Inventory.lean index fe3b3bd..129e5ed 100644 --- a/server/GameServer/Inventory.lean +++ b/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 => diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index e81bce4..59ecfc6 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/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 diff --git a/server/GameServer/Utils.lean b/server/GameServer/Utils.lean index 9891ecb..75e837e 100644 --- a/server/GameServer/Utils.lean +++ b/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 => diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 011a2fa..f0ae278 100644 --- a/server/lake-manifest.json +++ b/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", - "name": "std", + "rev": "51e6e0d24db9341fb031288c298b7e6b56102253", + "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"} diff --git a/server/lakefile.lean b/server/lakefile.lean index bf56c16..b73ef25 100644 --- a/server/lakefile.lean +++ b/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 diff --git a/server/lean-toolchain b/server/lean-toolchain index 9ad3040..ef1f67e 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0