diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index 6ad1578..e81bce4 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -1,6 +1,5 @@ import GameServer.EnvExtensions import GameServer.InteractiveGoal -import Std.Data.Array.Init.Basic import GameServer.Hints import I18n diff --git a/server/lake-manifest.json b/server/lake-manifest.json index 5210e4c..011a2fa 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -4,10 +4,10 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", + "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "v4.7.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", @@ -22,10 +22,19 @@ {"url": "https://github.com/hhu-adam/lean-i18n.git", "type": "git", "subDir": null, - "rev": "62dde5278a45771629f043e48effef44b4147ff8", + "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39", "name": "i18n", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.7.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.7.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "GameServer", diff --git a/server/lakefile.lean b/server/lakefile.lean index 2fd0de9..bf56c16 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -4,11 +4,13 @@ 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}" -def leanVersion := "v4.6.0" -- TODO +def leanVersion : String := s!"v{Lean.versionString}" require std from git "https://github.com/leanprover/std4.git" @ leanVersion -require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ "main" -- 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 + lean_lib GameServer diff --git a/server/lean-toolchain b/server/lean-toolchain index f96d662..9ad3040 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.1 +leanprover/lean4:v4.7.0