bump to v4.7.0

leanprover-community · Apr 10, 2024 · 67b03d9 · 67b03d9
1 parent a15dd0a
commit 67b03d9
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0