fix: packages dir path and repo url

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 :=

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 :=

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

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
     }