From 55fa486ce66acb53e44c9cdcf6fdd96c514c2ef9 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 11 Jan 2023 18:18:09 -0500 Subject: [PATCH] fix: packages dir path and repo url --- Lake/Config/Package.lean | 12 ++++++++---- Lake/Config/Workspace.lean | 13 +++++++------ Lake/Load/Main.lean | 14 +++++++------- Lake/Load/Materialize.lean | 6 +++--- 4 files changed, 25 insertions(+), 20 deletions(-) diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 2f4a6310b1..1999b4ea65 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -232,11 +232,15 @@ abbrev name (self : Package) : Name := self.opaqueDeps.map (·.get) /-- -The package's remote packages directory -(derived from its `packagesDir` configuration). +The package's remote packages directory. +Either its `packagesDir` configuration or `defaultPackagesDir`. -/ -def packagesDir (self : Package) : FilePath := - self.dir / self.config.packagesDir.getD defaultPackagesDir +def relPkgsDir (self : Package) : FilePath := + self.config.packagesDir.getD defaultPackagesDir + +/-- The package's `dir` joined with its `relPkgsDir` -/ +def pkgsDir (self : Package) : FilePath := + self.dir / self.relPkgsDir /-- The package's JSON manifest of remote dependencies. -/ def manifestFile (self : Package) : FilePath := diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 6c1eab0a88..7fddaee5d6 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -44,12 +44,13 @@ namespace Workspace @[inline] def config (self : Workspace) : WorkspaceConfig := self.root.config.toWorkspaceConfig -/-- -The workspace's remote packages directory -(derived from its `packagesDir` configuration). --/ -@[inline] def packagesDir (self : Workspace) : FilePath := - self.root.packagesDir +/-- The workspace's remote packages directory. -/ +@[inline] def relPkgsDir (self : Workspace) : FilePath := + self.root.relPkgsDir + +/-- The workspace's `dir` joined with its `relPkgsDir`. -/ +@[inline] def pkgsDir (self : Workspace) : FilePath := + self.root.pkgsDir /-- The workspace's Lake manifest. -/ @[inline] def manifestFile (self : Workspace) : FilePath := diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean index d954622ecb..ded245a8da 100644 --- a/Lake/Load/Main.lean +++ b/Lake/Load/Main.lean @@ -48,7 +48,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.dir ws.packagesDir entry + let result ← materializePackageEntry ws.dir ws.relPkgsDir entry modifyThe (NameMap MaterializeResult) (·.insert entry.name result) let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts let deps ← deps.mapM fun dep => do @@ -56,8 +56,8 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do return (dep, result) else let depName := dep.name.toString (escape := false) - let entry ← updateSource relPkgDir ws.packagesDir depName dep.src - let result ← materializePackageEntry ws.dir ws.packagesDir entry + let entry ← updateSource relPkgDir ws.relPkgsDir depName dep.src + let result ← materializePackageEntry ws.dir ws.relPkgsDir entry modifyThe (NameMap MaterializeResult) (·.insert entry.name result) return (dep, result) let depPkgs ← deps.mapM fun (dep, result) => do @@ -70,7 +70,7 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)} match res with | (.ok _, results) => - let mut manifest : Manifest := {packagesDir? := ws.packagesDir} + let mut manifest : Manifest := {packagesDir? := ws.relPkgsDir} for (_, result) in results do manifest := manifest.insert result.manifestEntry return manifest @@ -129,11 +129,11 @@ Resolving a workspace's dependencies using a manifest, downloading and/or updating them as necessary. -/ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) : LogIO Workspace := do - if !manifest.isEmpty && manifest.packagesDir? != some ws.packagesDir then + if !manifest.isEmpty && manifest.packagesDir? != some ws.relPkgsDir then logWarning <| "manifest out of date: package directory changed, " ++ "use `lake update` to update" - let packagesDir := manifest.packagesDir?.getD ws.packagesDir + let relPkgsDir := manifest.packagesDir?.getD ws.relPkgsDir let res ← EStateT.run' (mkNameMap Package) do buildAcyclic (·.name) ws.root fun pkg resolve => do let topLevel := pkg.name = ws.root.name @@ -156,7 +156,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) : LogIO Wor 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 ws.dir packagesDir entry + let result ← materializePackageEntry ws.dir relPkgsDir 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 938f7a5506..0852c6b907 100644 --- a/Lake/Load/Materialize.lean +++ b/Lake/Load/Materialize.lean @@ -66,7 +66,7 @@ structure MaterializeResult where /-- Materializes a package entry, cloning and/or checkout it out as necessary. -/ -def materializePackageEntry (wsDir packagesDir : FilePath) (manifestEntry : PackageEntry) : LogIO MaterializeResult := +def materializePackageEntry (wsDir relPkgsDir : FilePath) (manifestEntry : PackageEntry) : LogIO MaterializeResult := match manifestEntry with | .path _name pkgDir => return { @@ -77,7 +77,7 @@ def materializePackageEntry (wsDir packagesDir : FilePath) (manifestEntry : Pack manifestEntry } | .git name url rev _inputRev? subDir? => do - let relGitDir := packagesDir / name + let relGitDir := relPkgsDir / name let gitDir := wsDir / relGitDir let repo := GitRepo.mk gitDir /- @@ -96,7 +96,7 @@ def materializePackageEntry (wsDir packagesDir : FilePath) (manifestEntry : Pack return { pkgDir := wsDir / relPkgDir relPkgDir - remoteUrl? := url + remoteUrl? := Git.filterUrl? url gitTag? := ← repo.findTag? manifestEntry }