feat: lake leanOptions config entry

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

src/Lean/Util/ServerOptions.lean → 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)

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,15 +109,14 @@ def weakLeanArgs : Array String :=
     #[]
 
 package {pkgName} where
-  moreServerOptions := moreServerOptions
+  leanOptions := leanOptions
   -- add any package configuration options here
 
 require mathlib from git
   \"https://github.com/leanprover-community/mathlib4.git\"
 
 @[default_target]
 lean_lib {libRoot} where
-  moreLeanArgs := moreLeanArgs
   weakLeanArgs := weakLeanArgs
   -- add any library configuration options here
 "

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,

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`.

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.

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
 

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

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`, `<more|weak><Lean|Leanc|Link>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`, `<more|weak><Lean|Leanc|Link>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