diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean index c5502c2b0d..223fdbede8 100644 --- a/Lake/Load/Main.lean +++ b/Lake/Load/Main.lean @@ -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 diff --git a/Lake/Load/Materialize.lean b/Lake/Load/Materialize.lean index 7522344dc3..fea0e37b86 100644 --- a/Lake/Load/Materialize.lean +++ b/Lake/Load/Materialize.lean @@ -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?