From 34385b8ee8708c6f6c4cc4079a4d331f84c32682 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sat, 5 Apr 2025 09:38:35 -0400
Subject: [PATCH] feat: lake: use absolute paths (#7822)

This PR changes Lake to use normalized absolute paths for its various
files and directories.

This is done by storing absolute paths for the workspace directory,
package directories, and configuration files. These are then joined to
relative paths (e.g., for source directories) using a custom join
function that eliminates `.` paths.

Closes #7498. Closes #4042.
---
 src/lake/Lake/CLI/Error.lean                  |  6 ++--
 src/lake/Lake/CLI/Main.lean                   |  6 ++--
 src/lake/Lake/Config/Package.lean             | 11 +++---
 src/lake/Lake/Load/Config.lean                | 19 +++++-----
 src/lake/Lake/Load/Lean.lean                  |  1 +
 src/lake/Lake/Load/Package.lean               | 36 +++++++++----------
 src/lake/Lake/Load/Resolve.lean               |  4 +++
 src/lake/Lake/Load/Toml.lean                  |  1 +
 src/lake/Lake/Util/FilePath.lean              | 15 ++++++++
 src/lake/Lake/Util/IO.lean                    | 17 +++++++++
 .../deps/bar/lake-manifest.expected.json      |  8 ++---
 src/lake/examples/deps/test.sh                |  4 +--
 src/lake/tests/env/test.sh                    |  6 ++--
 .../tests/manifest/lake-manifest-latest.json  | 22 ++++++++++++
 src/lake/tests/manifest/test.sh               |  3 +-
 src/lake/tests/order/test.sh                  |  4 +--
 tests/pkg/test_extern/expected.txt            |  2 +-
 tests/pkg/test_extern/test.sh                 |  6 ++--
 18 files changed, 114 insertions(+), 57 deletions(-)
 create mode 100644 src/lake/tests/manifest/lake-manifest-latest.json

diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean
index 3e65607f24..218cd00578 100644
--- a/src/lake/Lake/CLI/Error.lean
+++ b/src/lake/Lake/CLI/Error.lean
@@ -47,11 +47,12 @@ inductive CliError
 | unknownLakeInstall
 | leanRevMismatch (expected actual : String)
 | invalidEnv (msg : String)
+| missingRootDir (path :  System.FilePath)
 deriving Inhabited, Repr
 
 namespace CliError
 
-def toString : CliError → String
+protected def toString : CliError → String
 | missingCommand          => "missing command"
 | unknownCommand cmd      => s!"unknown command '{cmd}'"
 | missingArg arg          => s!"missing {arg}"
@@ -83,5 +84,6 @@ def toString : CliError → String
 | unknownLakeInstall      => "could not detect the configuration of the Lake installation"
 | leanRevMismatch e a     => s!"expected Lean commit {e}, but got {if a.isEmpty then "nothing" else a}"
 | invalidEnv msg          => msg
+| missingRootDir p        => s!"workspace directory not found: {p}"
 
-instance : ToString CliError := ⟨toString⟩
+instance : ToString CliError := ⟨CliError.toString⟩
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index b961dbe62c..5e6e5248cb 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -75,11 +75,13 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
     opts.noCache |>.adaptExcept fun msg => .invalidEnv msg
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
-def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
+def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig := do
+  let some wsDir ← resolvePath? opts.rootDir
+    | throw <| .missingRootDir opts.rootDir
   return {
     lakeArgs? := opts.args.toArray
     lakeEnv := ← opts.computeEnv
-    wsDir := opts.rootDir
+    wsDir
     relConfigFile := opts.configFile
     packageOverrides := opts.packageOverrides
     lakeOpts := opts.configOpts
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 43822f5798..1c156e0c22 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -14,6 +14,7 @@ import Lake.Load.Config
 import Lake.Util.DRBMap
 import Lake.Util.OrdHashSet
 import Lake.Util.Version
+import Lake.Util.FilePath
 
 open System Lean
 
@@ -303,12 +304,14 @@ declare_opaque_type OpaquePostUpdateHook (pkg : Name)
 structure Package where
   /-- The name of the package. -/
   name : Name
-  /-- The path to the package's directory. -/
+  /-- The absolute path to the package's directory. -/
   dir : FilePath
   /-- The path to the package's directory relative to the workspace. -/
   relDir : FilePath
   /-- The package's user-defined configuration. -/
   config : PackageConfig name
+  /-- The absolute path to the package's configuration file. -/
+  configFile : FilePath
   /-- The path to the package's configuration file (relative to `dir`). -/
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
@@ -450,10 +453,6 @@ namespace Package
 @[inline] def pkgsDir (self : Package) : FilePath :=
   self.dir / self.relPkgsDir
 
-/-- The full path to the package's configuration file. -/
-@[inline] def configFile (self : Package) : FilePath :=
-  self.dir / self.relConfigFile
-
 /-- The path to the package's JSON manifest of remote dependencies. -/
 @[inline] def manifestFile (self : Package) : FilePath :=
   self.dir / self.relManifestFile
@@ -589,7 +588,7 @@ The package's `buildDir` joined with its `nativeLibDir` configuration.
   self.buildDir / self.config.nativeLibDir
 
 /-- The package's `buildDir` joined with its `nativeLibDir` configuration. -/
-@[deprecated "Use staticLibDir or sharedLibDir instead." (since := "2025-03-29")]
+@[inline, deprecated "Use staticLibDir or sharedLibDir instead." (since := "2025-03-29")]
 def nativeLibDir (self : Package) : FilePath :=
   self.buildDir / self.config.nativeLibDir
 
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index f1b6afb6e8..283117ddb4 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -8,6 +8,7 @@ import Lean.Data.Name
 import Lean.Data.Options
 import Lake.Config.Env
 import Lake.Load.Manifest
+import Lake.Util.FilePath
 
 namespace Lake
 open System Lean
@@ -22,12 +23,16 @@ structure LoadConfig where
   A value of `none` means that Lake is not restartable via the CLI.
   -/
   lakeArgs? : Option (Array String) := none
-  /-- The root directory of the Lake workspace. -/
+  /-- The absolute path to the root directory of the Lake workspace. -/
   wsDir : FilePath
-  /-- The directory of the loaded package (relative to the root). -/
+  /-- The loaded package's directory (relative to the workspace directory). -/
   relPkgDir : FilePath := "."
-  /-- The package's Lake configuration file (relative to the package directory). -/
+  /-- The absolute path to the loaded package's directory. -/
+  pkgDir : FilePath := wsDir / relPkgDir
+  /-- The package's Lake configuration file (relative to its directory). -/
   relConfigFile : FilePath := defaultConfigFile
+    /-- The full path to the loaded package's Lake configuration file. -/
+  configFile : FilePath := pkgDir / relConfigFile
   /-- Additional package overrides for this workspace load. -/
   packageOverrides : Array PackageEntry := #[]
   /-- A set of key-value Lake configuration options (i.e., `-K` settings). -/
@@ -48,14 +53,6 @@ structure LoadConfig where
   /-- The URL to this package's Git remote (if any). -/
   remoteUrl : String := ""
 
-/-- The full path to loaded package's directory. -/
-@[inline] def LoadConfig.pkgDir (cfg : LoadConfig) : FilePath :=
-  cfg.wsDir / cfg.relPkgDir
-
-/-- The full path to loaded package's configuration file. -/
-@[inline] def LoadConfig.configFile (cfg : LoadConfig) : FilePath :=
-  cfg.pkgDir / cfg.relConfigFile
-
 /-- The package's Lake directory (for Lake temporary files). -/
 @[inline] def LoadConfig.lakeDir (cfg : LoadConfig) : FilePath :=
   cfg.pkgDir / defaultLakeDir
diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean
index 7ecb42c0c7..99ec934068 100644
--- a/src/lake/Lake/Load/Lean.lean
+++ b/src/lake/Lake/Load/Lean.lean
@@ -29,6 +29,7 @@ def loadLeanConfig (cfg : LoadConfig)
     name, config
     dir := cfg.pkgDir
     relDir := cfg.relPkgDir
+    configFile := cfg.configFile
     relConfigFile := cfg.relConfigFile
     scope := cfg.scope
     remoteUrl := cfg.remoteUrl
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index c39380f7cb..6a84d3dbf8 100644
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -36,18 +36,12 @@ Otherwise, returns an empty string.
 -/
 def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
   if cfgFile.extension.isSome then
-    realPath cfgFile
+    resolvePath cfgFile
   else
-    let realLeanFile ← realPath (cfgFile.addExtension "lean")
-    if realLeanFile.toString.isEmpty then
-      realPath (cfgFile.addExtension "toml")
+    if let some path ← resolvePath? (cfgFile.addExtension "lean") then
+      return path
     else
-      return realLeanFile
-where
-  @[inline] realPath file := do
-    match (← (IO.FS.realPath file).toBaseIO) with
-    | .ok path => return if (← path.pathExists) then path else ""
-    | _ => return ""
+      resolvePath (cfgFile.addExtension "toml")
 
 /--
 Loads a Lake package configuration (either Lean or TOML).
@@ -57,8 +51,10 @@ def loadPackageCore
   (name : String) (cfg : LoadConfig)
 : LogIO (Package × Option Environment) := do
   if let some ext := cfg.relConfigFile.extension then
-    unless (← cfg.configFile.pathExists) do
-      error s!"{name}: configuration file not found: {cfg.configFile}"
+    let cfg ←
+      if let some configFile ← resolvePath? cfg.configFile then
+        pure {cfg with configFile}
+      else error s!"{name}: configuration file not found: {cfg.configFile}"
     match ext with
     | "lean" => (·.map id some) <$> loadLeanConfig cfg
     | "toml" => ((·,none)) <$> loadTomlConfig cfg
@@ -68,15 +64,17 @@ def loadPackageCore
     let relTomlFile := cfg.relConfigFile.addExtension "toml"
     let leanFile := cfg.pkgDir / relLeanFile
     let tomlFile := cfg.pkgDir / relTomlFile
-    let leanExists ← leanFile.pathExists
-    let tomlExists ← tomlFile.pathExists
-    if leanExists then
-      if tomlExists then
+    if let some configFile ← resolvePath? leanFile then
+      if (← tomlFile.pathExists) then
         logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
-      (·.map id some) <$> loadLeanConfig {cfg with relConfigFile := relLeanFile}
+       let cfg := {cfg with configFile, relConfigFile := relLeanFile}
+      let (pkg, env) ← loadLeanConfig cfg
+      return (pkg, some env)
     else
-      if tomlExists then
-        ((·,none)) <$> loadTomlConfig {cfg with relConfigFile := relTomlFile}
+      if let some configFile ← resolvePath? tomlFile then
+        let cfg := {cfg with configFile, relConfigFile := relTomlFile}
+        let pkg ← loadTomlConfig cfg
+        return (pkg, none)
       else
         error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
 
diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index 0f3122dae3..d636c112dc 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -43,9 +43,13 @@ def loadDepPackage
   (leanOpts : Options) (reconfigure : Bool)
 : StateT Workspace LogIO Package := fun ws => do
   let name := dep.name.toString (escape := false)
+  let pkgDir := ws.dir / dep.relPkgDir
+  let some pkgDir ← resolvePath? pkgDir
+    | error s!"{name}: package directory not found: {pkgDir}"
   let (pkg, env?) ← loadPackageCore name {
     lakeEnv := ws.lakeEnv
     wsDir := ws.dir
+    pkgDir
     relPkgDir := dep.relPkgDir
     relConfigFile := dep.configFile
     lakeOpts, leanOpts, reconfigure
diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean
index d5897a609a..99b829a417 100644
--- a/src/lake/Lake/Load/Toml.lean
+++ b/src/lake/Lake/Load/Toml.lean
@@ -433,6 +433,7 @@ def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
         name := name
         dir := cfg.pkgDir
         relDir := cfg.relPkgDir
+        configFile := cfg.configFile
         relConfigFile := cfg.relConfigFile
         scope := cfg.scope
         remoteUrl := cfg.remoteUrl
diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean
index 6a4a5d1032..aece8aa143 100644
--- a/src/lake/Lake/Util/FilePath.lean
+++ b/src/lake/Lake/Util/FilePath.lean
@@ -22,3 +22,18 @@ def mkRelPathString (path : FilePath) : String :=
 
 scoped instance : ToJson FilePath where
   toJson path := toJson <| mkRelPathString path
+
+/--
+Joins a two (potentially) relative paths.
+If either path is `.`, this returns the other.
+-/
+def joinRelative (a b : FilePath) : System.FilePath :=
+  if b == "." then a
+  else if a == "." then b
+  else inline FilePath.join a b
+
+scoped instance : Div FilePath where
+  div := joinRelative
+
+scoped instance : HDiv FilePath String FilePath where
+  hDiv p sub := joinRelative p ⟨sub⟩
diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean
index d38c06c7e9..19d7ea63b8 100644
--- a/src/lake/Lake/Util/IO.lean
+++ b/src/lake/Lake/Util/IO.lean
@@ -11,3 +11,20 @@ namespace Lake
 /-- Creates any missing parent directories of `path`. -/
 def createParentDirs (path : System.FilePath) : IO Unit := do
   if let some dir := path.parent then IO.FS.createDirAll dir
+
+/-- Returns the normalized real path of a file if it exists. Otherwise, returns `""`. -/
+def resolvePath (path : System.FilePath) : BaseIO System.FilePath := do
+  match (← (IO.FS.realPath path).toBaseIO) with
+  | .ok path =>
+    -- Real path does not guarentee the file exists on Windows
+    if (← path.pathExists) then
+      return path.normalize
+    else
+      return ""
+  | _ =>
+    return ""
+
+/-- Returns the normalized real path of a file if and only if it exists. -/
+@[inline] def resolvePath? (path : System.FilePath) : BaseIO (Option System.FilePath) := do
+  let path ← resolvePath path
+  return if path.toString.isEmpty then none else path
diff --git a/src/lake/examples/deps/bar/lake-manifest.expected.json b/src/lake/examples/deps/bar/lake-manifest.expected.json
index 068c60e836..ed5b2da883 100644
--- a/src/lake/examples/deps/bar/lake-manifest.expected.json
+++ b/src/lake/examples/deps/bar/lake-manifest.expected.json
@@ -6,28 +6,28 @@
    "name": "foo",
    "manifestFile": "lake-manifest.json",
    "inherited": false,
-   "dir": "./../foo",
+   "dir": "../foo",
    "configFile": "lakefile.lean"},
   {"type": "path",
    "scope": "",
    "name": "b",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
-   "dir": "./../foo/./../b",
+   "dir": "../foo/../b",
    "configFile": "lakefile.lean"},
   {"type": "path",
    "scope": "",
    "name": "a",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
-   "dir": "./../foo/./../a",
+   "dir": "../foo/../a",
    "configFile": "lakefile.lean"},
   {"type": "path",
    "scope": "",
    "name": "root",
    "manifestFile": "lake-manifest.json",
    "inherited": true,
-   "dir": "./../foo/./../b/./../root",
+   "dir": "../foo/../b/../root",
    "configFile": "lakefile.lean"}],
  "name": "bar",
  "lakeDir": ".lake"}
diff --git a/src/lake/examples/deps/test.sh b/src/lake/examples/deps/test.sh
index f319a0b10e..5265ef4901 100755
--- a/src/lake/examples/deps/test.sh
+++ b/src/lake/examples/deps/test.sh
@@ -10,7 +10,7 @@ $LAKE -d bar build --update
 # Serves as a regression test to ensure that multiples of a package in
 # the dependency tree do not produce duplicate entries in the manifest.
 # https://github.com/leanprover/lean4/pull/3957
-diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
+diff -u --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo build --update
 
 ./foo/.lake/build/bin/foo
@@ -34,7 +34,7 @@ test ! -d foo/.lake/build
 ./clean.sh
 
 $LAKE -d bar -f lakefile.toml build --update
-diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
+diff -u --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo -f lakefile.toml build --update
 
 ./foo/.lake/build/bin/foo
diff --git a/src/lake/tests/env/test.sh b/src/lake/tests/env/test.sh
index f833ce74ce..e26720e55e 100755
--- a/src/lake/tests/env/test.sh
+++ b/src/lake/tests/env/test.sh
@@ -18,10 +18,10 @@ $LAKE env printenv LEAN_GITHASH
 $LAKE env printenv LEAN_SYSROOT
 $LAKE env printenv LEAN_AR | grep --color ar
 $LAKE env printenv LEAN_PATH
-$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep --color examples/hello
+$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep --color hello
 $LAKE env printenv LEAN_SRC_PATH | grep --color lake
-$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep --color examples/hello
-$LAKE -d ../../examples/hello env printenv PATH | grep --color examples/hello
+$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep --color hello
+$LAKE -d ../../examples/hello env printenv PATH | grep --color hello
 
 # Test that `env` preserves the input environment for certain variables
 test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
diff --git a/src/lake/tests/manifest/lake-manifest-latest.json b/src/lake/tests/manifest/lake-manifest-latest.json
new file mode 100644
index 0000000000..a6e937ff8e
--- /dev/null
+++ b/src/lake/tests/manifest/lake-manifest-latest.json
@@ -0,0 +1,22 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "bar",
+   "type": "git",
+   "subDir": null,
+   "scope": "foo",
+   "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "foo",
+   "configFile": "lakefile.lean"}],
+ "name": "«foo-bar»",
+ "lakeDir": ".lake"}
diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh
index 6545ba4cff..08d6855d63 100755
--- a/src/lake/tests/manifest/test.sh
+++ b/src/lake/tests/manifest/test.sh
@@ -25,14 +25,13 @@ git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd
 
-LATEST_VER=v1.1.0
 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
 
 # Test an update produces the expected manifest of the latest version
 test_update() {
   $LAKE update
   sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-  diff --strip-trailing-cr lake-manifest-$LATEST_VER.json lake-manifest.json
+  diff --strip-trailing-cr lake-manifest-latest.json lake-manifest.json
 }
 
 # ---
diff --git a/src/lake/tests/order/test.sh b/src/lake/tests/order/test.sh
index 8a99b861d9..a627c3778b 100755
--- a/src/lake/tests/order/test.sh
+++ b/src/lake/tests/order/test.sh
@@ -25,10 +25,10 @@ $LAKE exe Y | grep --color root
 
 cp lake-manifest.json lake-manifest-1.json
 $LAKE update foo
-diff --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json
 
 # Tests that order does not change in the presence of dep manifests
 $LAKE -d foo update
 $LAKE -d bar update
 $LAKE update
-diff --strip-trailing-cr lake-manifest-1.json lake-manifest.json
+diff -u --strip-trailing-cr lake-manifest-1.json lake-manifest.json
diff --git a/tests/pkg/test_extern/expected.txt b/tests/pkg/test_extern/expected.txt
index 2ac13533aa..c77b606af6 100644
--- a/tests/pkg/test_extern/expected.txt
+++ b/tests/pkg/test_extern/expected.txt
@@ -1,4 +1,4 @@
-error: ././././TestExtern.lean:5:0: native implementation did not agree with reference implementation!
+error: TestExtern.lean:5:0: native implementation did not agree with reference implementation!
 Compare the outputs of:
 #eval Nat.not_add 4 5
  and
diff --git a/tests/pkg/test_extern/test.sh b/tests/pkg/test_extern/test.sh
index 33b24a7bb8..5c1522146b 100755
--- a/tests/pkg/test_extern/test.sh
+++ b/tests/pkg/test_extern/test.sh
@@ -12,13 +12,13 @@ rm -rf .lake/build
 
 # Function to process the output
 verify_output() {
-    # Normalize path separators from backslashes to forward slashes
-    sed 's#\\#/#g' |
     awk '/error: .*lean:/, /error: Lean exited/' |
+    # Remove system-specific path information from error
+    sed 's/error: .*TestExtern.lean:/error: TestExtern.lean:/g' |
     sed '/error: Lean exited/d'
 }
 
-lake build 2>&1 | verify_output > produced.txt
+${LAKE:-lake} build 2>&1 | verify_output > produced.txt
 
 # Compare the actual output with the expected output
 if diff --strip-trailing-cr -q produced.txt expected.txt > /dev/null; then