From 5aa58aac4c2e21709a7f79cbccee473799bf7c70 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/Process/Attributes.lean | 4 ++--
 DocGen4/Process/Base.lean       | 2 +-
 lakefile.lean                   | 4 ++--
 lean-toolchain                  | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

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..466da79 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" "dbbcfdd1780612d7455d7e78af1f4a3562f45beb"
     },
     {
       name := `lake
-      src := Source.git "https://github.com/leanprover/lake" "d961d8cfaa1c354c10f3fed55b32de85c205f4ab"
+      src := Source.git "https://github.com/leanprover/lake" "463c4f02a399dd296f9fa00b45a95792b70b6e48"
     }
   ]
 }
diff --git a/lean-toolchain b/lean-toolchain
index 4d9c593..7c4b4e3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-04-16
+leanprover/lean4:nightly-2022-05-21