diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean
index 6893e152fc7c..ccb05192b19c 100644
--- a/src/lake/Lake/CLI/Init.lean
+++ b/src/lake/Lake/CLI/Init.lean
@@ -16,6 +16,9 @@ open Git System
 /-- The default module of an executable in `std` package. -/
 def defaultExeRoot : Name := `Main
 
+/-- `elan` toolchain file name -/
+def toolchainFileName : FilePath := "lean-toolchain"
+
 def gitignoreContents :=
 s!"/{defaultLakeDir}
 "
diff --git a/src/lake/Lake/Config/Defaults.lean b/src/lake/Lake/Config/Defaults.lean
new file mode 100644
index 000000000000..d69071e749ce
--- /dev/null
+++ b/src/lake/Lake/Config/Defaults.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+namespace Lake
+
+/--
+The default directory to output Lake-related files
+(e.g., build artifacts, packages, caches, etc.).
+Currently not configurable.
+-/
+def defaultLakeDir : FilePath := ".lake"
+
+/-- The default setting for a `WorkspaceConfig`'s `packagesDir` option. -/
+def defaultPackagesDir : FilePath := "packages"
+
+/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
+def defaultConfigFile : FilePath := "lakefile.lean"
+
+/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
+def defaultManifestFile := "lake-manifest.json"
+
+/-- The default build directory for packages (i.e., `.lake/build`). -/
+def defaultBuildDir : FilePath := defaultLakeDir / "build"
+
+/-- The default Lean library directory for packages. -/
+def defaultLeanLibDir : FilePath := "lib"
+
+/-- The default native library directory for packages. -/
+def defaultNativeLibDir : FilePath := "lib"
+
+/-- The default binary directory for packages. -/
+def defaultBinDir : FilePath := "bin"
+
+/-- The default IR directory for packages. -/
+def defaultIrDir : FilePath := "ir"
diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean
index df8a322915c0..c8f402e8cdc4 100644
--- a/src/lake/Lake/Config/InstallPath.lean
+++ b/src/lake/Lake/Config/InstallPath.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Util.NativeLib
+import Lake.Config.Defaults
 
 open System
 namespace Lake
@@ -78,17 +79,17 @@ def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
 
-/-- Standard path of `lake` in a Lake installation. -/
-def lakeExe (buildHome : FilePath) :=
-  buildHome / "bin" / "lake" |>.addExtension FilePath.exeExtension
+/-- Lake executable file path. -/
+def lakeExe (binDir : FilePath) :=
+  FilePath.mk "lake" |>.addExtension FilePath.exeExtension
 
 /-- Path information about the local Lake installation. -/
 structure LakeInstall where
   home : FilePath
   srcDir := home
-  binDir := home / "build" / "bin"
-  libDir := home / "build" / "lib"
-  lake := lakeExe <| home / "build"
+  binDir := home / defaultBuildDir / defaultBinDir
+  libDir := home / defaultBuildDir / defaultLeanLibDir
+  lake := binDir / lakeExe
   deriving Inhabited, Repr
 
 /-- Construct a Lake installation co-located with the specified Lean installation. -/
@@ -97,7 +98,7 @@ def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where
   srcDir := lean.srcDir / "lake"
   binDir := lean.binDir
   libDir := lean.leanLibDir
-  lake := lakeExe lean.sysroot
+  lake := lean.binDir / lakeExe
 
 /-! ## Detection Functions -/
 
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 3ec5dbcde402..34e30c40901a 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Config.Opaque
+import Lake.Config.Defaults
 import Lake.Config.LeanLibConfig
 import Lake.Config.LeanExeConfig
 import Lake.Config.ExternLibConfig
@@ -26,25 +27,6 @@ Currently used for package and target names taken from the CLI.
 def stringToLegalOrSimpleName (s : String) : Name :=
   if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName
 
---------------------------------------------------------------------------------
-/-! # Defaults -/
---------------------------------------------------------------------------------
-
-/-- The default setting for a `PackageConfig`'s `buildDir` option. -/
-def defaultBuildDir : FilePath := "build"
-
-/-- The default setting for a `PackageConfig`'s `leanLibDir` option. -/
-def defaultLeanLibDir : FilePath := "lib"
-
-/-- The default setting for a `PackageConfig`'s `nativeLibDir` option. -/
-def defaultNativeLibDir : FilePath := "lib"
-
-/-- The default setting for a `PackageConfig`'s `binDir` option. -/
-def defaultBinDir : FilePath := "bin"
-
-/-- The default setting for a `PackageConfig`'s `irDir` option. -/
-def defaultIrDir : FilePath := "ir"
-
 --------------------------------------------------------------------------------
 /-! # PackageConfig -/
 --------------------------------------------------------------------------------
@@ -102,9 +84,9 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   /--
   The directory to which Lake should output the package's build results.
-  Defaults to `defaultLakeDir / defaultBuildDir` (i.e., `.lake/build`).
+  Defaults to `defaultBuildDir` (i.e., `.lake/build`).
   -/
-  buildDir : FilePath := defaultLakeDir / defaultBuildDir
+  buildDir : FilePath := defaultBuildDir
 
   /--
   The build subdirectory to which Lake should output the package's
diff --git a/src/lake/Lake/Config/WorkspaceConfig.lean b/src/lake/Lake/Config/WorkspaceConfig.lean
index 5b19019230e6..5c11972903de 100644
--- a/src/lake/Lake/Config/WorkspaceConfig.lean
+++ b/src/lake/Lake/Config/WorkspaceConfig.lean
@@ -3,20 +3,11 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Config.Defaults
 
 open System
 namespace Lake
 
-/--
-The default directory to output Lake-related files
-(e.g., build artifacts, packages, caches, etc.).
-Currently not configurable.
--/
-def defaultLakeDir : FilePath := ".lake"
-
-/-- The default setting for a `WorkspaceConfig`'s `packagesDir` option. -/
-def defaultPackagesDir : FilePath := "packages"
-
 /-- A `Workspace`'s declarative configuration. -/
 structure WorkspaceConfig where
   /--
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index 27dd34bd2eee..c6ad9cd4c930 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -5,21 +5,13 @@ Authors: Mac Malone
 -/
 import Lean.Data.Name
 import Lean.Data.Options
+import Lake.Config.Defaults
 import Lake.Config.Env
 import Lake.Util.Log
 
 namespace Lake
 open System Lean
 
-/-- `elan` toolchain file name -/
-def toolchainFileName : FilePath := "lean-toolchain"
-
-/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
-def defaultConfigFile : FilePath := "lakefile.lean"
-
-/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
-def defaultManifestFile := "lake-manifest.json"
-
 /-- Context for loading a Lake configuration. -/
 structure LoadConfig where
   /-- The Lake environment of the load process. -/