chore: update toolchain

DocGen4/Load.lean

@@ -19,7 +19,7 @@ the Lean search path with the path to the proper compiler from lean-toolchain
 as well as all the dependencies.
 -/
 def lakeSetup : IO (Except UInt32 Lake.Workspace) := do
-  let (leanInstall?, lakeInstall?) ← Lake.findInstall?
+  let (_, leanInstall?, lakeInstall?) ← Lake.findInstall?
   let config := Lake.mkLoadConfig.{0} {leanInstall?, lakeInstall?}
   match ←(EIO.toIO' config) with
   | .ok config =>
@@ -30,10 +30,10 @@ def lakeSetup : IO (Except UInt32 Lake.Workspace) := do
   | .error err =>
     throw <| IO.userError err.toString
 
-def envOfImports (imports : List Name) : IO Environment := do
+def envOfImports (imports : Array Name) : IO Environment := do
  importModules (imports.map (Import.mk · false)) Options.empty
 
-def loadInit (imports : List Name) : IO Hierarchy := do
+def loadInit (imports : Array Name) : IO Hierarchy := do
  let env ← envOfImports imports
  pure <| Hierarchy.fromArray env.header.moduleNames
 
@@ -55,6 +55,6 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
 
 def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
-  load <| .loadAll [`Init, `Lean, `Lake]
+  load <| .loadAll #[`Init, `Lean, `Lake]
 
 end DocGen4

DocGen4/Output/SourceLinker.lean

@@ -72,7 +72,7 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
   let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile
       |>.run (Lake.MonadLog.eio .normal)
       |>.toIO (fun _ => IO.userError "Failed to load lake manifest")
-  for pkg in manifest.entryArray do
+  for pkg in manifest.packages do
     match pkg with
     | .git _ _ _ url rev .. => gitMap := gitMap.insert pkg.name (getGithubBaseUrl url, rev)
     | .path _ _ _ path =>
@@ -89,7 +89,7 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
     else if root == `Lake then
       s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
     else
-      match ws.packageArray.find? (·.isLocalModule module) with
+      match ws.packages.find? (·.isLocalModule module) with
       | some pkg =>
         match gitMap.find? pkg.name with
         | some (baseUrl, commit) => s!"{baseUrl}/blob/{commit}/{path}.lean"

DocGen4/Process/Analyze.lean

@@ -84,10 +84,10 @@ def shouldRender : ModuleMember → Bool
 end ModuleMember
 
 inductive AnalyzeTask where
-| loadAll (load : List Name) : AnalyzeTask
+| loadAll (load : Array Name) : AnalyzeTask
-| loadAllLimitAnalysis (analyze : List Name) : AnalyzeTask
+| loadAllLimitAnalysis (analyze : Array Name) : AnalyzeTask
 
-def AnalyzeTask.getLoad : AnalyzeTask → List Name
+def AnalyzeTask.getLoad : AnalyzeTask → Array Name
 | loadAll load => load
 | loadAllLimitAnalysis load => load
 
@@ -110,7 +110,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
   let env ← getEnv
   let relevantModules := match task with
     | .loadAll _ => HashSet.fromArray env.header.moduleNames
-    | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis.toArray
+    | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis
   let allModules := env.header.moduleNames
 
   let mut res ← getAllModuleDocs relevantModules.toArray

Main.lean

@@ -11,7 +11,7 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
   return topLevelModules
 
 def runSingleCmd (p : Parsed) : IO UInt32 := do
-  let relevantModules := [p.positionalArg! "module" |>.as! String |> String.toName]
+  let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
   let res ← lakeSetup
   match res with
   | Except.ok ws =>

lakefile.lean

@@ -27,7 +27,7 @@ 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 modJob ← mod.leanBin.fetch
+  let modJob ← mod.leanArts.fetch
   let buildDir := (← getWorkspace).root.buildDir
   let docFile := mod.filePath (buildDir / "doc") "html"
   exeJob.bindAsync fun exeFile exeTrace => do

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0-rc1