From 72d28d198a1390cc9def3e0f0e0f07449754d8e3 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Thu, 16 Nov 2023 16:47:47 +0100 Subject: [PATCH] feat: lake `leanOptions` config entry --- src/Lean/Util/FileSetupInfo.lean | 4 +- .../{ServerOptions.lean => LeanOptions.lean} | 54 +++++++++---------- src/lake/Lake/CLI/Init.lean | 8 +-- src/lake/Lake/CLI/Serve.lean | 8 ++- src/lake/Lake/Config/LeanConfig.lean | 20 ++++--- src/lake/Lake/Config/LeanLib.lean | 25 ++++++++- src/lake/Lake/Config/Module.lean | 3 ++ src/lake/Lake/Config/Package.lean | 6 ++- src/lake/README.md | 7 +-- 9 files changed, 82 insertions(+), 53 deletions(-) rename src/Lean/Util/{ServerOptions.lean => LeanOptions.lean} (50%) diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean index 24d4eeb5e476a..50f5405d68cdb 100644 --- a/src/Lean/Util/FileSetupInfo.lean +++ b/src/Lean/Util/FileSetupInfo.lean @@ -1,9 +1,9 @@ -import Lean.Util.ServerOptions +import Lean.Util.LeanOptions /-- Information shared between Lake and Lean when calling `lake setup-file`. -/ structure Lean.FileSetupInfo where paths : LeanPaths - setupOptions : ServerOptions + setupOptions : LeanOptions deriving FromJson, ToJson diff --git a/src/Lean/Util/ServerOptions.lean b/src/Lean/Util/LeanOptions.lean similarity index 50% rename from src/Lean/Util/ServerOptions.lean rename to src/Lean/Util/LeanOptions.lean index 51447a08aa325..f1e03c78b2f44 100644 --- a/src/Lean/Util/ServerOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -3,83 +3,83 @@ import Lean.Util.Paths namespace Lean /-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag. -/ -inductive ServerOptionValue where +inductive LeanOptionValue where | ofString (s : String) | ofBool (b : Bool) | ofNat (n : Nat) deriving Inhabited, Repr -def ServerOptionValue.ofDataValue? : DataValue → Option ServerOptionValue +def LeanOptionValue.ofDataValue? : DataValue → Option LeanOptionValue | .ofString s => some (.ofString s) | .ofBool b => some (.ofBool b) | .ofNat n => some (.ofNat n) | _ => none -def ServerOptionValue.toDataValue : ServerOptionValue → DataValue +def LeanOptionValue.toDataValue : LeanOptionValue → DataValue | .ofString s => .ofString s | .ofBool b => .ofBool b | .ofNat n => .ofNat n -instance : KVMap.Value ServerOptionValue where - toDataValue := ServerOptionValue.toDataValue - ofDataValue? := ServerOptionValue.ofDataValue? +instance : KVMap.Value LeanOptionValue where + toDataValue := LeanOptionValue.toDataValue + ofDataValue? := LeanOptionValue.ofDataValue? -instance : Coe String ServerOptionValue where - coe := ServerOptionValue.ofString +instance : Coe String LeanOptionValue where + coe := LeanOptionValue.ofString -instance : Coe Bool ServerOptionValue where - coe := ServerOptionValue.ofBool +instance : Coe Bool LeanOptionValue where + coe := LeanOptionValue.ofBool -instance : Coe Nat ServerOptionValue where - coe := ServerOptionValue.ofNat +instance : Coe Nat LeanOptionValue where + coe := LeanOptionValue.ofNat -instance : FromJson ServerOptionValue where +instance : FromJson LeanOptionValue where fromJson? | (s : String) => Except.ok s | (b : Bool) => Except.ok b | (n : Nat) => Except.ok n - | _ => Except.error "invalid ServerOptionValue type" + | _ => Except.error "invalid LeanOptionValue type" -instance : ToJson ServerOptionValue where +instance : ToJson LeanOptionValue where toJson | (s : String) => s | (b : Bool) => b | (n : Nat) => n -/-- Formats the server option value as a CLI flag argument. -/ -def ServerOptionValue.asCliFlagValue : (v : ServerOptionValue) → String +/-- Formats the lean option value as a CLI flag argument. -/ +def LeanOptionValue.asCliFlagValue : (v : LeanOptionValue) → String | (s : String) => s!"\"{s}\"" | (b : Bool) => toString b | (n : Nat) => toString n -/-- Options that are used by the server as if they were passed using `-D`. -/ -structure ServerOptions where - values : RBMap Name ServerOptionValue Name.cmp +/-- Options that are used by Lean as if they were passed using `-D`. -/ +structure LeanOptions where + values : RBMap Name LeanOptionValue Name.cmp deriving Inhabited, Repr -def ServerOptions.toOptions (serverOptions : ServerOptions) : Options := Id.run do +def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do let mut options := KVMap.empty - for ⟨name, optionValue⟩ in serverOptions.values do + for ⟨name, optionValue⟩ in leanOptions.values do options := options.insert name optionValue.toDataValue return options -def ServerOptions.fromOptions? (options : Options) : Option ServerOptions := do +def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do let mut values := RBMap.empty for ⟨name, dataValue⟩ in options do - let optionValue ← ServerOptionValue.ofDataValue? dataValue + let optionValue ← LeanOptionValue.ofDataValue? dataValue values := values.insert name optionValue return ⟨values⟩ -instance : FromJson ServerOptions where +instance : FromJson LeanOptions where fromJson? | Json.obj obj => do let values ← obj.foldM (init := RBMap.empty) fun acc k v => do let optionValue ← fromJson? v return acc.insert k.toName optionValue return ⟨values⟩ - | _ => Except.error "invalid ServerOptions type" + | _ => Except.error "invalid LeanOptions type" -instance : ToJson ServerOptions where +instance : ToJson LeanOptions where toJson options := Json.obj <| options.values.fold (init := RBNode.leaf) fun acc k v => acc.insert (cmp := compare) k.toString (toJson v) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index b4e2916ea205a..93d80cf96e774 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -93,14 +93,11 @@ def mathConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL -def moreServerOptions : Array ServerOption := #[ +def leanOptions : Array LeanOption := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` ⟨`pp.proofs.withType, false⟩ ] --- These settings only apply during `lake build`, but not in VSCode editor. -def moreLeanArgs := moreServerOptions.map ServerOption.asCliArg - -- These are additional settings which do not affect the lake hash, -- so they can be enabled in CI and disabled locally or vice versa. -- Warning: Do not put any options here that actually change the olean files, @@ -112,7 +109,7 @@ def weakLeanArgs : Array String := #[] package {pkgName} where - moreServerOptions := moreServerOptions + leanOptions := leanOptions -- add any package configuration options here require mathlib from git @@ -120,7 +117,6 @@ require mathlib from git @[default_target] lean_lib {libRoot} where - moreLeanArgs := moreLeanArgs weakLeanArgs := weakLeanArgs -- add any library configuration options here " diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 6692a1dbea5e0..de1f497743b24 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -42,14 +42,12 @@ def setupFile (loadConfig : LoadConfig) (path : FilePath) (imports : List String loadDynlibPaths := dynlibs : LeanPaths } - let setupOptions : ServerOptions ← do + let setupOptions : LeanOptions ← do let some moduleName ← searchModuleNameOfFileName path ws.leanSrcPath | pure ⟨∅⟩ - let some (pkg, module) := ws.packages.findSome? fun pkg => do - pure (pkg, ← pkg.findModule? moduleName) + let some module := ws.findModule? moduleName | pure ⟨∅⟩ - let options := pkg.config.moreServerOptions ++ module.lib.config.moreServerOptions - |>.map fun opt => ⟨opt.name, opt.value⟩ + let options := module.serverOptions.map fun opt => ⟨opt.name, opt.value⟩ pure ⟨Lean.RBMap.fromArray options Lean.Name.cmp⟩ IO.println <| Json.compress <| toJson { paths, diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index e7b05abac80c2..1dd8cd4dcf78c 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -1,4 +1,4 @@ -import Lean.Util.ServerOptions +import Lean.Util.LeanOptions /- Copyright (c) 2022 Mac Malone. All rights reserved. @@ -82,14 +82,14 @@ def BuildType.leancArgs : BuildType → Array String | minSizeRel => #["-Os", "-DNDEBUG"] | release => #["-O3", "-DNDEBUG"] -/-- Option that is used by the server as if it was passed using `-D`. -/ -structure ServerOption where +/-- Option that is used by Lean as if it was passed using `-D`. -/ +structure LeanOption where name : Lean.Name - value : Lean.ServerOptionValue + value : Lean.LeanOptionValue deriving Inhabited, Repr -/-- Formats the server option as a CLI argument using the `-D` flag. -/ -def ServerOption.asCliArg (o : ServerOption) : String := +/-- Formats the lean option as a CLI argument using the `-D` flag. -/ +def LeanOption.asCliArg (o : LeanOption) : String := s!"-D{o.name}={o.value.asCliFlagValue}" /-- Configuration options common to targets that build modules. -/ @@ -100,6 +100,12 @@ structure LeanConfig where -/ buildType : BuildType := .release /-- + Additional options to pass to both the Lean language server + (i.e., `lean --server`) launched by `lake serve` and to `lean` + when compiling a module's Lean source files. + -/ + leanOptions : Array LeanOption := #[] + /-- Additional arguments to pass to `lean` when compiling a module's Lean source files. -/ @@ -125,7 +131,7 @@ structure LeanConfig where Additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. -/ - moreServerOptions : Array ServerOption := #[] + moreServerOptions : Array LeanOption := #[] /-- Additional arguments to pass to `leanc` when compiling a module's C source files generated by `lean`. diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index 50995f6549bf0..bb72de0b22c5c 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/src/lake/Lake/Config/LeanLib.lean @@ -87,6 +87,20 @@ Is true if either the package or the library have `precompileModules` set. @[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet (BuildJob FilePath)) := self.config.nativeFacets +/-- +The arguments to pass to `lean --server` when running the Lean language server. +`serverOptions` is the the accumulation of: +- the package's `leanOptions` +- the library's `leanOptions` +- the package's `moreServerOptions` +- the library's `moreServerOptions` +-/ +@[inline] def serverOptions (self : LeanLib) : Array LeanOption := + self.pkg.leanOptions + ++ self.config.leanOptions + ++ self.pkg.moreServerOptions + ++ self.config.moreServerOptions + /-- The build type for modules of this library. That is, the minimum of package's `buildType` and the library's `buildType`. @@ -103,10 +117,17 @@ then the default (which is C for now). Backend.orPreferLeft self.config.backend self.pkg.backend /-- The arguments to pass to `lean` when compiling the library's Lean files. -That is, the package's `moreLeanArgs` plus the library's `moreLeanArgs`. +`leanArgs` is the accumulation of: +- the package's `leanOptions` +- the library's `leanOptions` +- the package's `moreLeanArgs` +- the library's `moreLeanArgs` -/ @[inline] def leanArgs (self : LeanLib) : Array String := - self.pkg.moreLeanArgs ++ self.config.moreLeanArgs + self.pkg.leanOptions.map (·.asCliArg) + ++ self.config.leanOptions.map (·.asCliArg) + ++ self.pkg.moreLeanArgs + ++ self.config.moreLeanArgs /-- The arguments to weakly pass to `lean` when compiling the library's Lean files. diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index b4e7845b78454..9038d5d749a01 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/src/lake/Lake/Config/Module.lean @@ -101,6 +101,9 @@ def dynlibSuffix := "-1" @[inline] def dynlibFile (self : Module) : FilePath := self.pkg.nativeLibDir / nameToSharedLib self.dynlibName +@[inline] def serverOptions (self : Module) : Array LeanOption := + self.lib.serverOptions + @[inline] def buildType (self : Module) : BuildType := self.lib.buildType diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index ec0a073ea976f..5bd4c676b79a6 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -330,7 +330,7 @@ namespace Package self.config.moreGlobalServerArgs /-- The package's `moreServerOptions` configuration. -/ -@[inline] def moreServerOptions (self : Package) : Array ServerOption := +@[inline] def moreServerOptions (self : Package) : Array LeanOption := self.config.moreServerOptions /-- The package's `buildType` configuration. -/ @@ -341,6 +341,10 @@ namespace Package @[inline] def backend (self : Package) : Backend := self.config.backend +/-- The package's `leanOptions` configuration. -/ +@[inline] def leanOptions (self : Package) : Array LeanOption := + self.config.leanOptions + /-- The package's `moreLeanArgs` configuration. -/ @[inline] def moreLeanArgs (self : Package) : Array String := self.config.moreLeanArgs diff --git a/src/lake/README.md b/src/lake/README.md index da0c3d125f4b1..5633143ffcce9 100644 --- a/src/lake/README.md +++ b/src/lake/README.md @@ -166,9 +166,10 @@ Lake provides a large assortment of configuration options for packages. * `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. See the option's docstring for a complete example. * `precompileModules`: Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`. -* `moreServerOptions`: Additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. -* `moreGlobalServerArgs`: Additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition) +* `moreServerOptions`: An `Array` of additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`. +* `moreGlobalServerArgs`: An `Array` of additional arguments to pass to `lean --server` which apply both to this package and anything else in the same server session (e.g. when browsing other packages from the same session via go-to-definition) * `buildType`: The `BuildType` of targets in the package (see [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670)). One of `debug`, `relWithDebInfo`, `minSizeRel`, or `release`. Defaults to `release`. +* `leanOptions`: Additional options to pass to both the Lean language server (i.e., `lean --server`) launched by `lake serve` and to `lean` while compiling Lean source files. * `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. * `weakLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. Unlike `moreLeanArgs`, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild. They come *before* `moreLeanArgs`. * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes some flags based on the `buildType`, but you can change this by, for example, adding `-O0` and `-UNDEBUG`. @@ -208,7 +209,7 @@ lean_lib «target-name» where * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules. * `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet. * `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source). -* `precompileModules`, `buildType`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) +* `precompileModules`, `buildType`, `leanOptions`, `Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are precompiled, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest) ### Binary Executables