update Lean and mdgen

* to use `#guard_msgs` * mdgen has to be updated
leanprover-community · Apr 20, 2024 · 06d8d3f · 06d8d3f
1 parent 7119967
commit 06d8d3f
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
-   "rev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "inputRev": "v1.3.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean4-metaprogramming-book»",

diff --git a/lakefile.lean b/lakefile.lean
@@ -9,7 +9,7 @@ lean_lib «lean4-metaprogramming-book» where
   globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]
 
 require mdgen from git
-  "https://github.com/Seasawher/mdgen" @ "c501f6b8fa2502362bf94678d404857e46e2b65d"
+  "https://github.com/Seasawher/mdgen" @ "v1.3.0"
 
 def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   let out ← IO.Process.output {

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.7.0