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