From f942fb23d285e3eb056d9e9019ad1e23a313e68f Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 26 Feb 2024 09:57:09 -0500 Subject: [PATCH] fix: lake: detection of custom Lake build dir --- src/lake/Lake/CLI/Init.lean | 3 ++ src/lake/Lake/Config/Defaults.lean | 37 +++++++++++++++++++++++ src/lake/Lake/Config/InstallPath.lean | 15 ++++----- src/lake/Lake/Config/Package.lean | 24 ++------------- src/lake/Lake/Config/WorkspaceConfig.lean | 11 +------ src/lake/Lake/Load/Config.lean | 10 +----- 6 files changed, 53 insertions(+), 47 deletions(-) create mode 100644 src/lake/Lake/Config/Defaults.lean diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 6893e152fc7cc..ccb05192b19cd 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 0000000000000..d69071e749ce9 --- /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 df8a322915c0c..c8f402e8cdc42 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 3ec5dbcde402b..34e30c40901a4 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 5b19019230e60..5c11972903dee 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 27dd34bd2eeea..c6ad9cd4c9309 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. -/