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

@@ -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⟩

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

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
 

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

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

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}"
 

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

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

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⟩

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

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"}

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

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

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"}

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
 }
 
 # ---

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

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

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