chore: reduce imports

This commit is contained in:
Gabriel Ebner 2022-11-23 16:00:35 -08:00 committed by Mac
parent 42a8e0f190
commit 733f015c65
2 changed files with 8 additions and 8 deletions

View file

@ -49,7 +49,7 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do
for entry in (← Manifest.loadOrEmpty pkg.manifestFile) do
unless (← getThe (NameMap MaterializeResult)).contains entry.name do
let entry := entry.inDirectory relPkgDir
let result ← materializePackageEntry ws.root entry
let result ← materializePackageEntry ws.root.dir ws.root.config.packagesDir entry
modifyThe (NameMap MaterializeResult) (·.insert entry.name result)
let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
let deps ← deps.mapM fun dep => do
@ -58,7 +58,7 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do
else
let depName := dep.name.toString (escape := false)
let entry ← updateSource relPkgDir ws.root.packagesDir depName dep.src
let result ← materializePackageEntry ws.root entry
let result ← materializePackageEntry ws.root.dir ws.root.config.packagesDir entry
modifyThe (NameMap MaterializeResult) (·.insert entry.name result)
return (dep, result)
let depPkgs ← deps.mapM fun (dep, result) => do
@ -106,7 +106,7 @@ def Package.materializeDeps (root : Package) : LogIO Package := do
let .some entry := manifest.find? dep.name
| error <| s!"dependency {dep.name} of {pkg.name} not in manifest, " ++
"use `lake update` to update"
let result ← materializePackageEntry root entry
let result ← materializePackageEntry root.dir root.config.packagesDir entry
loadDepPackage pkg result dep
return { pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·) }
match res with

View file

@ -66,19 +66,19 @@ structure MaterializeResult where
/--
Materializes a package entry, cloning and/or checkout it out as necessary.
-/
def materializePackageEntry (rootPkg : Package) (manifestEntry : PackageEntry) : LogIO MaterializeResult :=
def materializePackageEntry (rootPkgDir packagesDir : FilePath) (manifestEntry : PackageEntry) : LogIO MaterializeResult :=
match manifestEntry with
| .path _name pkgDir =>
return {
pkgDir := rootPkg.dir / pkgDir
pkgDir := rootPkgDir / pkgDir
relPkgDir := pkgDir
remoteUrl? := none
gitTag? := none
manifestEntry
}
| .git name url rev _inputRev? subDir? => do
let relGitDir := rootPkg.config.packagesDir / name
let gitDir := rootPkg.dir / relGitDir
let relGitDir := packagesDir / name
let gitDir := rootPkgDir / relGitDir
let repo := GitRepo.mk gitDir
/-
Do not update (fetch remote) if already on revision
@ -94,7 +94,7 @@ def materializePackageEntry (rootPkg : Package) (manifestEntry : PackageEntry) :
updateGitRepo repo url rev name
let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
return {
pkgDir := rootPkg.dir / relPkgDir
pkgDir := rootPkgDir / relPkgDir
relPkgDir
remoteUrl? := url
gitTag? := ← repo.findTag?