Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: lake: eager logging when materializing deps #6225

Merged
merged 1 commit into from
Nov 26, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions src/lake/Lake/Load/Resolve.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 :=
Expand Down Expand Up @@ -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
Expand All @@ -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 <|
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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; \
Expand Down
Loading