From 2ff48210268587e5506e1f51757f7eef2aabaac4 Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 7 Nov 2023 13:07:29 -0500 Subject: [PATCH] refactor: `.lake` directory for Lake outputs --- src/lake/Lake/CLI/Actions.lean | 1 - src/lake/Lake/CLI/Init.lean | 4 +--- src/lake/Lake/Config/InstallPath.lean | 10 +++++----- src/lake/Lake/Config/Package.lean | 18 +++++++++++++----- src/lake/Lake/Config/Workspace.lean | 8 ++++++++ src/lake/Lake/Config/WorkspaceConfig.lean | 13 ++++++++++--- src/lake/Lake/Load/Elab.lean | 7 +++++-- src/lake/Lake/Load/Main.lean | 19 ++++++++++++------- src/lake/Lake/Load/Manifest.lean | 12 +++++++----- src/lake/README.md | 12 ++++++------ 10 files changed, 67 insertions(+), 37 deletions(-) diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean index bd99ea6c12..3ef604a9f9 100644 --- a/src/lake/Lake/CLI/Actions.lean +++ b/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} diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 016c9cf56b..820da18156 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/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 := diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index 93c95c0099..e599f87add 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/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 `/build/bin/lake`. +the executable is located at `/.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 `/build/bin/lake` and its static -library and `.olean` files in `/build/lib`, and its source files -located directly in ``. +That is, with its binary located at `/.lake/build/bin/lake` and its +static library and `.olean` files in `/.lake/build/lib`, and +its source files located directly in ``. -/ def findLakeInstall? : BaseIO (Option LakeInstall) := do if let some home ← IO.getEnv "LAKE_HOME" then diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 5b8dd411ce..2855ee2484 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/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 := diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index 935cca4101..6dbd2dc2ba 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/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 diff --git a/src/lake/Lake/Config/WorkspaceConfig.lean b/src/lake/Lake/Config/WorkspaceConfig.lean index fdd00a3b8b..5b19019230 100644 --- a/src/lake/Lake/Config/WorkspaceConfig.lean +++ b/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 diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean index 7917bf670e..b4ec76233e 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/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 diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index 1c33f24286..2665eaed79 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/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 - diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean index c664adc926..8d9b6f1d3e 100644 --- a/src/lake/Lake/Load/Manifest.lean +++ b/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⟩ diff --git a/src/lake/README.md b/src/lake/README.md index dfc9f15c5c..f51078393f 100644 --- a/src/lake/README.md +++ b/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 `/bin`, their Lean libraries in `/lib/lean`, Lean's source files in `/src/lean`, and Lake's source files in `/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 `/build/bin/lake` with its Lean libraries at `/build/lib` and its sources directly in ``. +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 `/bin`, their Lean libraries in `/lib/lean`, Lean's source files in `/src/lean`, and Lake's source files in `/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/build/bin/lake` with its Lean libraries at `/.lake/build/lib` and its sources directly in ``. 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).