From 1d2ca29f2a54fa3111fdbf9d5ec0c97a8d9bf23a Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 24 Jul 2022 02:47:22 -0400 Subject: [PATCH] chore: remove package config builtin targets --- Lake/Build/Index.lean | 12 --- Lake/CLI/Build.lean | 23 +----- Lake/CLI/Init.lean | 5 +- Lake/Config/LeanExe.lean | 8 +- Lake/Config/LeanLib.lean | 4 - Lake/Config/Package.lean | 132 +-------------------------------- Lake/Load/Package.lean | 3 - examples/hello/lakefile.lean | 2 + examples/scripts/lakefile.lean | 3 +- test/62/test.sh | 4 +- 10 files changed, 14 insertions(+), 182 deletions(-) diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 81e7764927..623e456a4a 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -122,23 +122,14 @@ export BuildInfo (build buildIn) @[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget := self.lean.target -@[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget := - self.builtinLib.leanTarget - /-! ### Native Lean Lib Targets -/ @[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget := self.static.target.withInfo self.sharedLibFile -@[inline] protected def Package.staticLibTarget (self : Package) : FileTarget := - self.builtinLib.staticLibTarget - @[inline] protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget := self.shared.target.withInfo self.sharedLibFile -@[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget := - self.builtinLib.sharedLibTarget - /-! ### Lean Executable Targets -/ @[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget := @@ -149,6 +140,3 @@ export BuildInfo (build buildIn) @[inline] protected def LeanExe.target (self : LeanExe) : FileTarget := self.exe.target.withInfo self.file - -@[inline] protected def Package.exeTarget (self : Package) : FileTarget := - self.builtinExe.target diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 7af8d33441..4f981ed9e0 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -8,14 +8,6 @@ import Lake.CLI.Error namespace Lake -def Package.defaultTarget (self : Package) : OpaqueTarget := - match self.defaultFacet with - | .exe => self.exeTarget.withoutInfo - | .staticLib => self.staticLibTarget.withoutInfo - | .sharedLib => self.sharedLibTarget.withoutInfo - | .leanLib => self.leanLibTarget.withoutInfo - | .none => Target.nil - def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package := if spec.isEmpty then return ws.root @@ -86,23 +78,12 @@ def resolveTargetInPackage (ws : Workspace) (pkg : Package) (target : Name) (fac throw <| CliError.missingTarget pkg.name (target.toString false) def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError OpaqueTarget := - if pkg.defaultTargets.isEmpty then - return pkg.defaultTarget - else - return Target.collectOpaqueArray <| ← - pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous) + return Target.collectOpaqueArray <| ← + pkg.defaultTargets.mapM (resolveTargetInPackage ws pkg · .anonymous) def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError OpaqueTarget := if facet.isAnonymous then resolveDefaultPackageTarget ws pkg - else if facet == `exe then - return pkg.exeTarget.withoutInfo - else if facet == `staticLib then - return pkg.staticLibTarget.withoutInfo - else if facet == `sharedLib then - return pkg.sharedLibTarget.withoutInfo - else if facet == `leanLib then - return pkg.leanLibTarget.withoutInfo else if let some config := ws.findPackageFacetConfig? facet then do let some target := config.toTarget? (pkg.facet facet) rfl | throw <| CliError.nonTargetFacet "package" facet diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean index 651082abed..4a88b4a1a8 100644 --- a/Lake/CLI/Init.lean +++ b/Lake/CLI/Init.lean @@ -11,6 +11,9 @@ import Lake.Load.Config namespace Lake 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" @@ -25,7 +28,7 @@ def libFileContents := s!"def hello := \"world\"" def mainFileName : FilePath := - s!"{defaultBinRoot}.lean" + s!"{defaultExeRoot}.lean" def mainFileContents (libRoot : Name) := s!"import {libRoot} diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean index 5bcd138af4..7920b73253 100644 --- a/Lake/Config/LeanExe.lean +++ b/Lake/Config/LeanExe.lean @@ -20,10 +20,6 @@ structure LeanExe where @[inline] def Package.leanExes (self : Package) : Array LeanExe := self.leanExeConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[] -/-- The Lean executable built into the package. -/ -@[inline] def Package.builtinExe (self : Package) : LeanExe := - ⟨self, self.builtinExeConfig⟩ - /-- Try to find a Lean executable in the package with the given name. -/ @[inline] def Package.findLeanExe? (name : Name) (self : Package) : Option LeanExe := self.leanExeConfigs.find? name |>.map (⟨self, ·⟩) @@ -86,6 +82,4 @@ end LeanExe /-- Locate the named module in the package (if it is buildable and local to it). -/ def Package.findModule? (mod : Name) (self : Package) : Option Module := self.leanLibs.findSome? (·.findModule? mod) <|> - self.leanExes.findSome? (·.isRoot? mod) <|> - self.builtinLib.findModule? mod <|> - self.builtinExe.isRoot? mod + self.leanExes.findSome? (·.isRoot? mod) diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index 73d77f5c65..903405588a 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -20,10 +20,6 @@ structure LeanLib where @[inline] def Package.leanLibs (self : Package) : Array LeanLib := self.leanLibConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[] -/-- The Lean library built into the package. -/ -@[inline] def Package.builtinLib (self : Package) : LeanLib := - ⟨self, self.builtinLibConfig⟩ - /-- Try to find a Lean library in the package with the given name. -/ @[inline] def Package.findLeanLib? (name : Name) (self : Package) : Option LeanLib := self.leanLibConfigs.find? name |>.map (⟨self, ·⟩) diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 5ff682cb34..50e75ed9e4 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -35,23 +35,6 @@ def defaultOleanDir : FilePath := defaultLibDir /-- The default setting for a `PackageConfig`'s `irDir` option. -/ def defaultIrDir : FilePath := "ir" -/-- The default setting for a `PackageConfig`'s `binRoot` option. -/ -def defaultBinRoot : Name := `Main - --------------------------------------------------------------------------------- -/-! # PackageFacet -/ --------------------------------------------------------------------------------- - -/-- A buildable component of a `Package`. -/ -inductive PackageFacet -| /-- The package's binary executable. -/ exe -| /-- The package's static library. -/ staticLib -| /-- The package's shared library. -/ sharedLib -| /-- The package's lean library (e.g. `olean` / `ilean` files). -/ leanLib -| /-- The package has no buildable component. -/ none -deriving BEq, DecidableEq, Repr -instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩ - -------------------------------------------------------------------------------- /-! # PackageConfig -/ -------------------------------------------------------------------------------- @@ -72,17 +55,6 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where -/ extraDepTarget : Option OpaqueTarget := none - /-- - The optional `PackageFacet` to build on a bare `lake build` of the package. - Can be one of `exe`, `leanLib`, `staticLib`, `sharedLib`, or `none`. - Defaults to `exe`. See `lake help build` for more info on build facets. - - **DEPRECATED:** - Package facets will be removed in a future version of Lake. - Use a separate `lean_lib` or `lean_exe` default target instead. - -/ - defaultFacet : PackageFacet := .exe - /-- Whether to compile each of the package's module into a native shared library that is loaded whenever the module is imported. This speeds up evaluation of @@ -128,26 +100,6 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where -/ oleanDir : FilePath := defaultOleanDir - /-- - The root module(s) of the package's library. - - Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered - part of the package. - - Defaults to a single root of the package's upper camel case `name`. - -/ - libRoots : Array Name := #[toUpperCamelCase name] - - /-- - An `Array` of module `Glob`s to build for the package's library. - Defaults to a `Glob.one` of each of the module's `libRoots`. - - Submodule globs build every source file within their directory. - Local imports of glob'ed files (i.e., fellow modules of the package) are - also recursively built. - -/ - libGlobs : Array Glob := libRoots.map Glob.one - /-- The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). @@ -155,85 +107,20 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where -/ irDir : FilePath := defaultIrDir - /-- - The name of the package's static library. - Defaults to the package's upper camel case `name`. - -/ - libName : String := toUpperCamelCase name |>.toString (escape := false) - /-- The build subdirectory to which Lake should output the package's static library. Defaults to `defaultLibDir` (i.e., `lib`). -/ libDir : FilePath := defaultLibDir - /-- - The name of the package's binary executable. - Defaults to the package's `name` with any `.` replaced with a `-`. - -/ - binName : String := name.toStringWithSep "-" (escape := false) - /-- The build subdirectory to which Lake should output the package's binary executable. Defaults to `defaultBinDir` (i.e., `bin`). -/ binDir : FilePath := defaultBinDir - /-- - The root module of the package's binary executable. - Defaults to `defaultBinRoot` (i.e., `Main`). - - The root is built by recursively building its - local imports (i.e., fellow modules of the workspace). - - This setting is most useful for packages that are distributing both a - library and a binary (like Lake itself). In such cases, it is common for - there to be code (e.g., `main`) that is needed for the binary but should - not be included in the library proper. - -/ - binRoot : Name := defaultBinRoot - - /-- - Additional library `FileTarget`s (beyond the package's and its dependencies' - Lean libraries) to build and link to the package's binaries (and to dependent - packages' binaries). - - **DEPRECATED:** Use separate `extern_lib` targets instead. - -/ - moreLibTargets : Array FileTarget := #[] - - /-- - Whether to expose symbols within the executable to the Lean interpreter. - This allows the executable to interpret Lean files (e.g., via - `Lean.Elab.runFrontend`). - - Implementation-wise, this passes `-rdynamic` to the linker when building - on non-Windows systems. - - Defaults to `false`. - -/ - supportInterpreter : Bool := false - deriving Inhabited -namespace PackageConfig - -/-- The configuration of the package's library. -/ -def toLeanLibConfig (self : PackageConfig) : LeanLibConfig where - name := self.libName - roots := self.libRoots - globs := self.libGlobs - toLeanConfig := self.toLeanConfig - -/-- The configuration of the package's binary executable. -/ -def toLeanExeConfig (self : PackageConfig) : LeanExeConfig where - root := self.binRoot - name := self.binName - supportInterpreter := self.supportInterpreter - toLeanConfig := self.toLeanConfig - -end PackageConfig - -------------------------------------------------------------------------------- /-! # Package -/ -------------------------------------------------------------------------------- @@ -289,10 +176,6 @@ namespace Package @[inline] def extraDepTarget (self : Package) : OpaqueTarget := self.config.extraDepTarget.getD Target.nil -/-- The package's `defaultFacet` configuration. -/ -@[inline] def defaultFacet (self : Package) : PackageFacet := - self.config.defaultFacet - /-- The package's `precompileModules` configuration. -/ @[inline] def precompileModules (self : Package) : Bool := self.config.precompileModules @@ -349,25 +232,14 @@ namespace Package @[inline] def binDir (self : Package) : FilePath := self.buildDir / self.config.binDir -/-- The library configuration built into the package configuration. -/ -@[inline] def builtinLibConfig (self : Package) : LeanLibConfig := - self.config.toLeanLibConfig - -/-- The binary executable configuration built into the package configuration. -/ -@[inline] def builtinExeConfig (self : Package) : LeanExeConfig := - self.config.toLeanExeConfig - /-- Whether the given module is considered local to the package. -/ def isLocalModule (mod : Name) (self : Package) : Bool := - self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod) || - self.builtinLibConfig.isLocalModule mod + self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod) /-- Whether the given module is in the package (i.e., can build it). -/ def isBuildableModule (mod : Name) (self : Package) : Bool := self.leanLibConfigs.any (fun _ lib => lib.isBuildableModule mod) || - self.leanExeConfigs.any (fun _ exe => exe.root == mod) || - self.builtinLibConfig.isBuildableModule mod || - self.config.binRoot == mod + self.leanExeConfigs.any (fun _ exe => exe.root == mod) /-- Remove the package's build outputs (i.e., delete its build directory). -/ def clean (self : Package) : IO PUnit := do diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean index 4a11948751..e74d23992a 100644 --- a/Lake/Load/Package.lean +++ b/Lake/Load/Package.lean @@ -80,9 +80,6 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package := if self.config.extraDepTarget.isSome then logWarning <| "`extraDepTarget` has been deprecated. " ++ "Try to use a custom target or raise an issue about your use case." - if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && self.defaultFacet ≠ .none then - logWarning <| "Package targets are deprecated. " ++ - "Add a `lean_exe` and/or `lean_lib` default target to the package instead." -- Fill in the Package return {self with diff --git a/examples/hello/lakefile.lean b/examples/hello/lakefile.lean index d51a593cd1..dbf493210f 100644 --- a/examples/hello/lakefile.lean +++ b/examples/hello/lakefile.lean @@ -3,6 +3,8 @@ open Lake DSL package hello +lean_lib Hello + @[defaultTarget] lean_exe hello { root := `Main diff --git a/examples/scripts/lakefile.lean b/examples/scripts/lakefile.lean index ad45317e0b..513df8ec90 100644 --- a/examples/scripts/lakefile.lean +++ b/examples/scripts/lakefile.lean @@ -1,8 +1,7 @@ import Lake open Lake DSL -package scripts where - defaultFacet := .none +package scripts /-- Display a greeting diff --git a/test/62/test.sh b/test/62/test.sh index 8b5a6515de..7fe1b12cb5 100755 --- a/test/62/test.sh +++ b/test/62/test.sh @@ -5,8 +5,8 @@ set -euxo pipefail command -v elan > /dev/null || (echo "elan not found; skipping test"; exit 0) ./clean.sh -lake +leanprover/lean4:4.0.0-m3 new foo +lake +leanprover/lean4:nightly-2022-06-30 new foo cd foo -lake +leanprover/lean4:4.0.0-m3 build | grep -m1 foo +lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo cp ../../../lean-toolchain lean-toolchain ${LAKE:-../../../build/bin/lake} build | grep -m1 foo