refactor: .lake directory for Lake outputs

src/lake/Lake/CLI/Actions.lean

@@ -24,6 +24,5 @@ def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
   if let some repo := pkg.releaseRepo? then
     args := args.append #["-R", repo]
   tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile
-    (excludePaths := #["*.tar.gz", "*.tar.gz.trace"])
   logInfo s!"Uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}

src/lake/Lake/CLI/Init.lean

@@ -17,9 +17,7 @@ open Git System
 def defaultExeRoot : Name := `Main
 
 def gitignoreContents :=
-s!"/{defaultBuildDir}
-/{defaultConfigFile.withExtension "olean"}
-/{defaultPackagesDir}/*
+s!"/{defaultLakeDir}
 "
 
 def basicFileContents :=

src/lake/Lake/Config/InstallPath.lean

@@ -210,10 +210,10 @@ def findLakeLeanJointHome? : BaseIO (Option FilePath) := do
 
 /--
 Attempt to detect a specified Lake's executable's home by assuming
-the executable is located at `<lake-home>/build/bin/lake`.
+the executable is located at `<lake-home>/.lake/build/bin/lake`.
 -/
 def lakePackageHome? (lake : FilePath) : Option FilePath := do
-  (← (← lake.parent).parent).parent
+  (← (← (← lake.parent).parent).parent).parent
 
 /--
 Attempt to detect Lean's installation by first checking the
@@ -233,9 +233,9 @@ first checking the `LAKE_HOME` environment variable
 and then by trying the `lakePackageHome?` of the running executable.
 
 It assumes that the Lake installation is organized the same way it is built.
-That is, with its binary located at `<lake-home>/build/bin/lake` and its static
-library and `.olean` files in `<lake-home>/build/lib`, and its source files
-located directly in `<lake-home>`.
+That is, with its binary located at `<lake-home>/.lake/build/bin/lake` and its
+static library and `.olean` files in `<lake-home>/.lake/build/lib`, and
+its source files located directly in `<lake-home>`.
 -/
 def findLakeInstall? : BaseIO (Option LakeInstall) := do
   if let some home ← IO.getEnv "LAKE_HOME" then

src/lake/Lake/Config/Package.lean

@@ -115,9 +115,9 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
 
   /--
   The directory to which Lake should output the package's build results.
-  Defaults to `defaultBuildDir` (i.e., `build`).
+  Defaults to `defaultLakeDir / defaultBuildDir` (i.e., `.lake/build`).
   -/
-  buildDir : FilePath := defaultBuildDir
+  buildDir : FilePath := defaultLakeDir / defaultBuildDir
 
   /--
   The build subdirectory to which Lake should output the package's
@@ -264,11 +264,19 @@ namespace Package
 @[inline] def deps (self : Package) : Array Package  :=
   self.opaqueDeps.map (·.get)
 
+/-- The path to the package's Lake directory relative to `dir` (e.g., `.lake`). -/
+@[inline] def relLakeDir (_ : Package) : FilePath :=
+  defaultLakeDir
+
+/-- The full path to the package's Lake directory (i.e, `dir` joined with `relLakeDir`). -/
+@[inline] def lakeDir (self : Package) : FilePath :=
+  self.dir / self.relLakeDir
+
 /-- The path for storing the package's remote dependencies relative to `dir` (i.e., `packagesDir`). -/
 @[inline] def relPkgsDir (self : Package) : FilePath :=
   self.config.packagesDir
 
-/-- The package's `dir` joined with its `relPkgsDir` -/
+/-- The package's `dir` joined with its `relPkgsDir`. -/
 @[inline] def pkgsDir (self : Package) : FilePath :=
   self.dir / self.relPkgsDir
 
@@ -296,9 +304,9 @@ namespace Package
 @[inline] def buildArchive (self : Package) : String :=
   nameToArchive self.buildArchive?
 
-/-- The package's `buildDir` joined with its `buildArchive` configuration. -/
+/-- The package's `lakeDir` joined with its `buildArchive` configuration. -/
 @[inline] def buildArchiveFile (self : Package) : FilePath :=
-  self.buildDir / self.buildArchive
+  self.lakeDir / self.buildArchive
 
 /-- The package's `preferReleaseBuild` configuration. -/
 @[inline] def preferReleaseBuild (self : Package) : Bool :=

src/lake/Lake/Config/Workspace.lean

@@ -46,6 +46,14 @@ namespace Workspace
 @[inline] def config (self : Workspace) : WorkspaceConfig :=
   self.root.config.toWorkspaceConfig
 
+/-- The path to the workspace' Lake directory relative to `dir`. -/
+@[inline] def relLakeDir (self : Workspace) : FilePath :=
+  self.root.relLakeDir
+
+/-- The the full path to the workspace's Lake directory (e.g., `.lake`). -/
+@[inline] def lakeDir (self : Workspace) : FilePath :=
+  self.root.lakeDir
+
 /-- The path to the workspace's remote packages directory relative to `dir`. -/
 @[inline] def relPkgsDir (self : Workspace) : FilePath :=
   self.root.relPkgsDir

src/lake/Lake/Config/WorkspaceConfig.lean

@@ -7,14 +7,21 @@ Authors: Mac Malone
 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 := "lake-packages"
+def defaultPackagesDir : FilePath := "packages"
 
 /-- A `Workspace`'s declarative configuration. -/
 structure WorkspaceConfig where
   /--
   The directory to which Lake should download remote dependencies.
-  Defaults to `defaultPackagesDir` (i.e., `lake-packages`).
+  Defaults to `defaultLakeDir / defaultPackagesDir` (i.e., `.lake/packages`).
   -/
-  packagesDir : FilePath := defaultPackagesDir
+  packagesDir : FilePath := defaultLakeDir / defaultPackagesDir
   deriving Inhabited, Repr

src/lake/Lake/Load/Elab.lean

@@ -83,9 +83,11 @@ Import the OLean for the configuration file if `reconfigure` is not set
 and an up-to-date one exists (i.e., one newer than the configuration and the
 toolchain). Otherwise, elaborate the configuration and save it to the OLean.
 -/
-def importConfigFile (wsDir pkgDir : FilePath) (lakeOpts : NameMap String)
+def importConfigFile (wsDir pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
 (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do
-  let olean := configFile.withExtension "olean"
+  let some configName := FilePath.mk <$> configFile.fileName
+    | error "invalid configuration file name"
+  let olean := lakeDir / configName.withExtension "olean"
   let useOLean ← id do
     if reconfigure then return false
     let .ok oleanMTime ← getMTime olean |>.toBaseIO | return false
@@ -118,6 +120,7 @@ def importConfigFile (wsDir pkgDir : FilePath) (lakeOpts : NameMap String)
           env := extDescrs[entryIdx]!.addEntry env ent
     return env
   else
+    IO.FS.createDirAll lakeDir
     let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
     Lean.writeModule env olean
     return env

src/lake/Lake/Load/Main.lean

@@ -30,10 +30,11 @@ def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array
 Elaborate a dependency's configuration file into a `Package`.
 The resulting package does not yet include any dependencies.
 -/
-def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
+def MaterializedDep.loadPackage (dep : MaterializedDep) (wsDir : FilePath)
 (leanOpts : Options) (lakeOpts : NameMap String) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
-  let configEnv ← importConfigFile wsDir dir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
+  let lakeDir := dir / defaultLakeDir
+  let configEnv ← importConfigFile wsDir dir lakeDir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
     dir, config, configEnv, leanOpts
@@ -46,7 +47,8 @@ Does not resolve dependencies.
 -/
 def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.env.leanSearchPath
-  let configEnv ← importConfigFile config.rootDir config.rootDir
+  let configEnv ← importConfigFile
+    config.rootDir config.rootDir (config.rootDir / defaultLakeDir)
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let root := {
@@ -115,7 +117,7 @@ def Workspace.updateAndMaterialize (ws : Workspace)
           return (pkg, dep.relPkgDir)
         else
           -- Load the package
-          let depPkg ← loadDepPackage ws.dir dep pkg.leanOpts dep.opts reconfigure
+          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts dep.opts reconfigure
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
@@ -131,7 +133,11 @@ def Workspace.updateAndMaterialize (ws : Workspace)
   match res with
   | (.ok root, deps) =>
     let ws : Workspace ← {ws with root}.finalize
-    let manifest : Manifest := {name? := ws.root.name, packagesDir? := ws.relPkgsDir}
+    let manifest : Manifest := {
+      name? := ws.root.name
+      lakeDir? := ws.relLakeDir
+      packagesDir? := ws.relPkgsDir
+    }
     let manifest := ws.packages.foldl (init := manifest) fun manifest pkg =>
       match deps.find? pkg.name with
       | some dep => manifest.addPackage dep.manifestEntry
@@ -182,7 +188,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
           let result ← entry.materialize ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
           -- Union manifest and configuration options (preferring manifest)
           let opts := entry.opts.mergeBy (fun _ e _ => e) dep.opts
-          loadDepPackage ws.dir result pkg.leanOpts opts reconfigure
+          result.loadPackage ws.dir pkg.leanOpts opts reconfigure
         else if topLevel then
           error <|
             s!"dependency '{dep.name}' not in manifest; " ++
@@ -221,4 +227,3 @@ def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
   discard <| ws.updateAndMaterialize toUpdate rc
-

src/lake/Lake/Load/Manifest.lean

@@ -54,6 +54,7 @@ end PackageEntry
 /-- Manifest data structure that is serialized to the file. -/
 structure Manifest where
   name? : Option Name := none
+  lakeDir? : Option FilePath := none
   packagesDir? : Option FilePath := none
   packages : Array PackageEntry := #[]
 
@@ -72,11 +73,12 @@ instance : ForIn m Manifest PackageEntry where
   forIn self init f := self.packages.forIn init f
 
 protected def toJson (self : Manifest) : Json :=
-  Json.mkObj <| .join [
-    [("version", version)],
-    Json.opt "name" self.name?,
-    [("packagesDir", toJson self.packagesDir?)],
-    [("packages", toJson self.packages)]
+  Json.mkObj [
+    ("version", version),
+    ("name", toJson self.name?),
+    ("lakeDir", toJson self.lakeDir?),
+    ("packagesDir", toJson self.packagesDir?),
+    ("packages", toJson self.packages)
   ]
 
 instance : ToJson Manifest := ⟨Manifest.toJson⟩

src/lake/README.md

@@ -54,7 +54,7 @@ $ cd hello
 Either way, Lake will create the following template directory structure and initialize a Git repository for the package.
 
 ```
-build/         # Lake build outputs
+.lake/         # Lake output directory
 Hello/         # library source files; accessible via `import Hello.*`
   Basic.lean   # an example library module file
   ...          # additional files should be added here
@@ -110,12 +110,12 @@ lean_exe «hello» where
   supportInterpreter := true
 ```
 
-The command `lake build` is used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `build/bin`. The command `lake clean` deletes `build`.
+The command `lake build` is used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `.lake/build/bin`. The command `lake clean` deletes `build`.
 
 ```
 $ lake build
 ...
-$ ./build/bin/hello
+$ ./.lake/build/bin/hello
 Hello, world!
 ```
 
@@ -153,7 +153,7 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Layout
 
-* `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `lake-packages`.
+* `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `.lake/packages`.
 * `manifestFile`: The path of a package's manifest file, which stores the exact versions of its resolved dependencies. Defaults to `lake-manifest.json`.
 * `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.)
 * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.
@@ -380,7 +380,7 @@ Otherwise, there is a pre-packaged `build.sh` shell script that can be used to b
 $ ./build.sh -j4
 ```
 
-After building, the `lake` binary will be located at `build/bin/lake` and the library's `.olean` files will be located in `build/lib`.
+After building, the `lake` binary will be located at `.lake/build/bin/lake` and the library's `.olean` files will be located in `.lake/build/lib`.
 
 ### Building with Nix Flakes
 
@@ -390,6 +390,6 @@ Lake is built as part of the main Lean 4 flake at the repository root.
 
 The `lake` executable needs to know where to find the Lean library files (e.g., `.olean`, `.ilean`) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and `lean`.
 
-Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in `<sysroot>/bin`, their Lean libraries in `<sysroot>/lib/lean`, Lean's source files in `<sysroot>/src/lean`, and Lake's source files in `<sysroot>/src/lean/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `<lake-home>/build/bin/lake` with its Lean libraries at `<lake-home>/build/lib` and its sources directly in `<lake-home>`.
+Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located under their shared sysroot. In particular, their binaries are located in `<sysroot>/bin`, their Lean libraries in `<sysroot>/lib/lean`, Lean's source files in `<sysroot>/src/lean`, and Lake's source files in `<sysroot>/src/lean/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `<lake-home>/.lake/build/bin/lake` with its Lean libraries at `<lake-home>/.lake/build/lib` and its sources directly in `<lake-home>`.
 
 This search path can be augmented by including other directories of Lean libraries in the `LEAN_PATH` environment variable (and their sources in `LEAN_SRC_PATH`). This can allow the user to correct Lake's search when the files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important during development, as this prevents the Lake version used to build Lake from using the Lake version being built's Lean libraries (instead of its own) to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors).