chore: update to 4.8

DocGen4/LeanInk/Output.lean

@@ -129,26 +129,26 @@ def Message.toHtml (m : Message) : AlectryonM Html := do
     </blockquote>
 
 def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
-  let messages :=
+  let messages ← do
     if s.messages.size > 0 then
-      #[
+      pure #[
         <div class="alectryon-messages">
           [← s.messages.mapM Message.toHtml]
         </div>
       ]
     else
-      #[]
-  
-  let goals :=
+      pure #[]
+
+  let goals ←
     if s.goals.size > 0 then
       -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
-      #[
+      pure #[
         <div class="alectryon-goals">
           [← s.goals.mapM Goal.toHtml]
         </div>
       ]
     else
-      #[]
+      pure #[]
 
   let buttonLabel ← getNextButtonLabel
 

DocGen4/Output/Module.lean

@@ -114,15 +114,15 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
     else
       #[]
-  let leanInkHtml :=
+  let leanInkHtml ← do
     if ← leanInkEnabled? then
-      #[
+      pure #[
         <div class="ink_link">
           <a href={← declNameToInkLink doc.getName}>ink</a>
         </div>
       ]
     else
-      #[]
+      pure #[]
 
   pure
     <div class="decl" id={doc.getName.toString}>

DocGen4/Output/Navbar.lean

@@ -29,12 +29,11 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
   let dirNodes ← dirs.mapM moduleListDir
   let fileNodes ← files.mapM moduleListFile
   let moduleLink ← moduleNameToLink h.getName
-  let summary :=
+  let summary ← do
     if h.isFile then
-      <summary>{s!"{h.getName.getString!} ({<a href={← moduleNameToLink h.getName}>file</a>})"} </summary>
+      pure <summary>{s!"{h.getName.getString!} ({<a href={← moduleNameToLink h.getName}>file</a>})"} </summary>
     else
-      <summary>{h.getName.getString!}</summary>
-
+      pure <summary>{h.getName.getString!}</summary>
   pure
     <details class="nav_sect" "data-path"={moduleLink} [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
       {summary}

DocGen4/Output/Structure.lean

@@ -31,20 +31,22 @@ def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
 Render all information about a structure as HTML.
 -/
 def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
-  let structureHtml :=
+  let structureHtml ← do
     if Name.isSuffixOf `mk i.ctor.name then
-      (<ul class="structure_fields" id={i.ctor.name.toString}>
-        [← i.fieldInfo.mapM fieldToHtml]
-      </ul>)
+      pure
+        <ul class="structure_fields" id={i.ctor.name.toString}>
+          [← i.fieldInfo.mapM fieldToHtml]
+        </ul>
     else
       let ctorShortName := i.ctor.name.componentsRev.head!.toString
-      (<ul class="structure_ext">
-        <li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
-        <ul class="structure_ext_fields">
-          [← i.fieldInfo.mapM fieldToHtml]
+      pure
+        <ul class="structure_ext">
+          <li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
+          <ul class="structure_ext_fields">
+            [← i.fieldInfo.mapM fieldToHtml]
+          </ul>
+          <li class="structure_ext_ctor">)</li>
         </ul>
-        <li class="structure_ext_ctor">)</li>
-      </ul>)
   return #[structureHtml]
 
 end Output

DocGen4/Process/Attributes.lean

@@ -1,4 +1,5 @@
 import Lean
+import Lean.ReducibilityAttrs
 
 namespace DocGen4
 
@@ -86,7 +87,7 @@ instance : ToString ReducibilityStatus where
 The list of all enum based attributes doc-gen knows about and can recover.
 -/
 @[reducible]
-def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩]
 
 instance : ToString ExternEntry where
   toString entry :=
@@ -127,8 +128,8 @@ def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAtt
 def getParametricValues (decl : Name) : MetaM (Array String) := do
   let mut uniform ← getValues decl parametricAttributes
   -- This attribute contains an `Option Name` but we would like to pretty print it better
-  if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
-    let str := match depTag with
+  if let some depEntry := Linter.deprecatedAttr.getParam? (← getEnv) decl then
+    let str := match depEntry.newName? with
     | some alt => s!"deprecated {alt.toString}"
     | none => "deprecated"
     uniform := uniform.push str
@@ -155,11 +156,19 @@ def hasCsimp (decl : Name) : MetaM (Option String) := do
   else
     return none
 
+def getReducibility (decl : Name) : MetaM (Option String) := do
+  let status ← getReducibilityStatus decl
+  match status with
+  | .reducible => return some "reducible"
+  | .irreducible => return some "irreducible"
+  -- This is the default so we don't print it.
+  | .semireducible => return none
+
 /--
 The list of custom attributes, that don't fit in the parametric or enum
 attribute kinds, doc-gen konws about and can recover.
 -/
-def customAttrs := #[hasSimp, hasCsimp]
+def customAttrs := #[hasSimp, hasCsimp, getReducibility]
 
 def getCustomAttrs (decl : Name) : MetaM (Array String) := do
   let mut values := #[]

DocGen4/Process/DocInfo.lean

@@ -137,7 +137,7 @@ def isProjFn (declName : Name) : MetaM Bool := do
     if isStructure env parent then
       match getStructureInfo? env parent with
       | some i =>
-        match i.fieldNames.find? (· == name) with
+        match i.fieldNames.find? (·.toString == name) with
         | some _ => return true
         | none => return false
       | none => panic! s!"{parent} is not a structure"

DocGen4/Process/InstanceInfo.lean

@@ -21,9 +21,9 @@ def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
   return names
 where
   findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit
-    | (.default, .sort .zero) => modify (·.push "_builtin_prop")
-    | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu")
-    | (.default, .sort _) => modify (·.push "_builtin_sortu")
+    | (.default, .sort .zero) => modify (·.push `_builtin_prop)
+    | (.default, .sort (.succ _)) => modify (·.push `_builtin_typeu)
+    | (.default, .sort _) => modify (·.push `_builtin_sortu)
     | (.default, e) =>
       match e.getAppFn with
       | .const name .. => modify (·.push name)

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/xubaiw/CMark.lean",
    "type": "git",
    "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
    "name": "CMark",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+   "rev": "10d88b52fa8d717fa8e29af3abf0c3a2bf175497",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly",

lakefile.lean

@@ -63,8 +63,8 @@ def appendModPath (libUri : String) (pathSep : Char) (mod : Module)  : String :=
 /--
 Append the library and mod path to the given Uri referring to the package source.
 -/
-def appendLibModPath (pkgUri : String) (pathSep : Char) (lib : LeanLibConfig) (mod : Module) : String :=
-  let libPath := filteredPath lib.srcDir
+def appendLibModPath (pkgUri : String) (pathSep : Char) (mod : Module) : String :=
+  let libPath := filteredPath mod.lib.srcDir
   appendModPath (pathSep.toString.intercalate (pkgUri :: libPath)) pathSep mod
 
 /--
@@ -87,79 +87,69 @@ def getGithubBaseUrl (url : String) : Option String :=
   else
     .none
 
-def getGithubUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
-  let url ←  getGitRemoteUrl pkg.dir "origin"
+def getGithubUrl (mod : Module) : IO String := do
+  let url ← getGitRemoteUrl mod.pkg.dir "origin"
   let .some baseUrl := getGithubBaseUrl url
       | throw <| IO.userError <|
         s!"Could not interpret Git remote uri {url} as a Github source repo.\n"
           ++ "See README on source URIs for more details."
-  let commit ← getProjectCommit pkg.dir
-  let srcDir := filteredPath pkg.config.srcDir
+  let commit ← getProjectCommit mod.pkg.dir
+  let srcDir := filteredPath mod.pkg.config.srcDir
   let pkgUri := "/".intercalate <| baseUrl :: "blob" :: commit :: srcDir
-
-  pure <| appendLibModPath pkgUri '/' lib mod
+  return appendLibModPath pkgUri '/' mod
 
 /--
 Return a File uri for the module.
 -/
-def getFileUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) := do
-  let dir ← IO.FS.realPath (pkg.dir / pkg.config.srcDir)
-  pure <| appendLibModPath s!"file://{dir}" FilePath.pathSeparator lib mod
+def getFileUri (mod : Module) : IO String := do
+  let dir ← IO.FS.realPath (mod.pkg.dir / mod.pkg.config.srcDir)
+  return appendLibModPath s!"file://{dir}" FilePath.pathSeparator mod
 
 /--
 Return a VSCode uri for the module.
 -/
-def getVSCodeUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
-  let dir ← IO.FS.realPath (pkg.dir / pkg.config.srcDir)
-  pure <| appendLibModPath s!"vscode://file/{dir}" FilePath.pathSeparator lib mod
+def getVSCodeUri (mod : Module) : IO String := do
+  let dir ← IO.FS.realPath (mod.pkg.dir / mod.pkg.config.srcDir)
+  return appendLibModPath s!"vscode://file/{dir}" FilePath.pathSeparator mod
 
 /--
 Attempt to determine URI to use for the module source file.
 -/
-def getSrcUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
+def getSrcUri (mod : Module) : IO String := do
   match ←IO.getEnv "DOCGEN_SRC" with
-  | .none | .some "github" | .some "" => getGithubUrl pkg lib mod
-  | .some "vscode" => getVSCodeUri pkg lib mod
-  | .some "file" => getFileUri pkg lib mod
+  | .none | .some "github" | .some "" => getGithubUrl mod
+  | .some "vscode" => getVSCodeUri mod
+  | .some "file" => getFileUri mod
   | .some _ => throw <| IO.userError "$DOCGEN_SRC should be github, file, or vscode."
 
 module_facet docs (mod) : FilePath := do
-  let some docGen4 ← findLeanExe? `«doc-gen4»
-    | error "no doc-gen4 executable configuration found in workspace"
-  let exeJob ← docGen4.exe.fetch
+  let exeJob ← «doc-gen4».fetch
   let modJob ← mod.leanArts.fetch
-  let ws ← getWorkspace
-  let pkg ← ws.packages.find? (·.isLocalModule mod.name)
-  let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
   -- Build all documentation imported modules
   let imports ← mod.imports.fetch
   let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
-  let srcUri ← getSrcUri pkg libConfig mod
-  let buildDir := ws.root.buildDir
+  let srcUri ← getSrcUri mod
+  let buildDir := (←getWorkspace).root.buildDir
   let docFile := mod.filePath (buildDir / "doc") "html"
   depDocJobs.bindAsync fun _ depDocTrace => do
   exeJob.bindAsync fun exeFile exeTrace => do
   modJob.bindSync fun _ modTrace => do
     let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
     let trace ← buildFileUnlessUpToDate docFile depTrace do
-      logStep s!"Documenting module: {mod.name}"
       proc {
         cmd := exeFile.toString
         args := #["single", mod.name.toString, srcUri]
         env := ← getAugmentedEnv
       }
     return (docFile, trace)
 
--- TODO: technically speaking this facet does not show all file dependencies
+-- TODO: technically speaking this target does not show all file dependencies
 target coreDocs : FilePath := do
-  let some docGen4 ← findLeanExe? `«doc-gen4»
-    | error "no doc-gen4 executable configuration found in workspace"
-  let exeJob ← docGen4.exe.fetch
+  let exeJob ← «doc-gen4».fetch
   let basePath := (←getWorkspace).root.buildDir / "doc"
   let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
   exeJob.bindSync fun exeFile exeTrace => do
     let trace ← buildFileUnlessUpToDate dataFile exeTrace do
-      logStep "Documenting Lean core: Init and Lean"
       proc {
         cmd := exeFile.toString
         args := #["genCore"]
@@ -170,7 +160,7 @@ target coreDocs : FilePath := do
 library_facet docs (lib) : FilePath := do
   let mods ← lib.modules.fetch
   let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
-  let coreJob : BuildJob FilePath ← coreDocs.fetch
+  let coreJob ← coreDocs.fetch
   let exeJob ← «doc-gen4».fetch
   -- Shared with DocGen4.Output
   let basePath := (←getWorkspace).root.buildDir / "doc"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1