From e8fb9a7f0fbcbff4338ffd73266c8cb6a9c413bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 21 May 2022 12:50:55 +0200
Subject: [PATCH] chore: update to latest nightly

---
 DocGen4/Load.lean               | 1 +
 DocGen4/Process/Attributes.lean | 4 ++--
 DocGen4/Process/Base.lean       | 2 +-
 lakefile.lean                   | 4 ++--
 lean-toolchain                  | 2 +-
 5 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 09d2d5c..704751d 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -6,6 +6,7 @@ Authors: Henrik Böving
 
 import Lean
 import Lake
+import Lake.CLI.Main
 import DocGen4.Process
 import Std.Data.HashMap
 
diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean
index d69f79c..02dc67d 100644
--- a/DocGen4/Process/Attributes.lean
+++ b/DocGen4/Process/Attributes.lean
@@ -28,7 +28,7 @@ structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
 /--
 Obtain the value of an enum attribute for a certain name.
 -/
-def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := do
   let val ← EnumAttributes.getValue attr env decl
   some (toString val)
 
@@ -38,7 +38,7 @@ instance : ValueAttr EnumAttributes where
 /--
 Obtain the value of a parametric attribute for a certain name.
 -/
-def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
   let val ← ParametricAttribute.getParam attr env decl
   some (attr.attr.name.toString ++ " " ++ toString val)
 
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index 592368c..5527036 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -167,7 +167,7 @@ inductive DocInfo where
 Turns an `Expr` into a pretty printed `CodeWithInfos`.
 -/
 def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
-  let (fmt, infos) ← formatInfos expr
+  let (fmt, infos) ←  PrettyPrinter.ppExprWithInfos expr
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
     env := ← getEnv
diff --git a/lakefile.lean b/lakefile.lean
index d7d73b6..f2d17bb 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,11 +15,11 @@ package «doc-gen4» {
     },
     {
       name := `Cli
-      src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3"
+      src := Source.git "https://github.com/mhuisi/lean4-cli" "159a20e5e165b1bbe070594b5969d8147241bb04"
     },
     {
       name := `lake
-      src := Source.git "https://github.com/leanprover/lake" "d961d8cfaa1c354c10f3fed55b32de85c205f4ab"
+      src := Source.git "https://github.com/leanprover/lake" "cb0eab4cbcfe58090b3c739e1e90982804597704"
     }
   ]
 }
diff --git a/lean-toolchain b/lean-toolchain
index 4d9c593..533511f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-04-16
+leanprover/lean4:nightly-2022-05-27