diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index d56f4bc79848..fcbd367c38e7 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -146,7 +146,7 @@ Also, move the packages directory if its location has changed. -/ private def reuseManifest (ws : Workspace) (toUpdate : NameSet) -: UpdateT LogIO PUnit := do +: UpdateT LoggerIO PUnit := do let rootName := ws.root.name.toString (escape := false) match (← Manifest.load ws.manifestFile |>.toBaseIO) with | .ok manifest => @@ -174,7 +174,7 @@ private def reuseManifest logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}" /-- Add a package dependency's manifest entries to the update state. -/ -private def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do +private def addDependencyEntries (pkg : Package) : UpdateT LoggerIO PUnit := do match (← Manifest.load pkg.manifestFile |>.toBaseIO) with | .ok manifest => manifest.packages.forM fun entry => do @@ -189,7 +189,7 @@ private def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do /-- Materialize a single dependency, updating it if desired. -/ private def updateAndMaterializeDep (ws : Workspace) (pkg : Package) (dep : Dependency) -: UpdateT LogIO MaterializedDep := do +: UpdateT LoggerIO MaterializedDep := do if let some entry ← fetch? dep.name then entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir else @@ -210,7 +210,7 @@ private def updateAndMaterializeDep /-- Verify that a dependency was loaded with the correct name. -/ private def validateDep (pkg : Package) (dep : Dependency) (matDep : MaterializedDep) (depPkg : Package) -: LogIO PUnit := do +: LoggerIO PUnit := do if depPkg.name ≠ dep.name then if dep.name = .mkSimple "std" then let rev := @@ -352,7 +352,7 @@ where @[inline] updateAndLoadDep pkg dep := do let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep loadUpdatedDep pkg dep matDep - @[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LogIO) Package := do + @[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LoggerIO) Package := do let depPkg ← loadDepPackage matDep dep.opts leanOpts true validateDep pkg dep matDep depPkg addDependencyEntries depPkg @@ -361,7 +361,7 @@ where /-- Write package entries to the workspace manifest. -/ def Workspace.writeManifest (ws : Workspace) (entries : NameMap PackageEntry) -: LogIO PUnit := do +: IO PUnit := do let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg => match entries.find? pkg.name with | some entry => arr.push <| @@ -376,7 +376,7 @@ def Workspace.writeManifest manifest.saveToFile ws.manifestFile /-- Run a package's `post_update` hooks. -/ -def Package.runPostUpdateHooks (pkg : Package) : LakeT LogIO PUnit := do +def Package.runPostUpdateHooks (pkg : Package) : LakeT LoggerIO PUnit := do unless pkg.postUpdateHooks.isEmpty do logInfo s!"{pkg.name}: running post-update hooks" pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg @@ -405,7 +405,7 @@ reporting warnings and/or errors as appropriate. -/ def validateManifest (pkgEntries : NameMap PackageEntry) (deps : Array Dependency) -: LogIO PUnit := do +: LoggerIO PUnit := do if pkgEntries.isEmpty && !deps.isEmpty then error "missing manifest; use `lake update` to generate one" deps.forM fun dep => do @@ -429,7 +429,7 @@ downloading and/or updating them as necessary. def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (leanOpts : Options := {}) (reconfigure := false) -: LogIO Workspace := do +: LoggerIO Workspace := do if !manifest.packages.isEmpty && manifest.packagesDir? != some (mkRelPathString ws.relPkgsDir) then logWarning <| "manifest out of date: packages directory changed; \