Merge pull request #54 from leanprover/update

Update to latest nightly

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
 

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)
 

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

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"
     }
   ]
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-04-16
+leanprover/lean4:nightly-2022-05-27