feat: replace __args__ with get_config? + related refactors

Lake/CLI/Help.lean

@@ -19,6 +19,7 @@ OPTIONS:
   --dir, -d=file        use the package configuration in a specific directory
   --file, -f=file       use a specific file for the package configuration
   --lean=cmd            specify the `lean` command used by Lake
+  -K key[=value]        set the configuration file option named key
 
 COMMANDS:
   new <name> [<temp>]   create a Lean package in a new directory
@@ -60,7 +61,7 @@ def helpBuild :=
 "Build targets
 
 USAGE:
-  lake build [<targets>...] [-- <args>...]
+  lake build [<targets>...]
 
 A target is specified with a string of the form:
 
@@ -96,18 +97,16 @@ TARGET EXAMPLES:        build the ...
   :exe                  root package's executable
 
 A bare `build` command will build the default facet of the root package.
-Arguments to the `Packager` itself can be specified with `args`.
 Package dependencies are not updated during a build."
 
 def helpUpdate :=
 "Update dependencies
 
 USAGE:
-  lake update [-- <args>...]
+  lake update
 
 This command sets up the directory with the package's dependencies
 (i.e., `packagesDir`, which is, by default, `lean_packages`).
-Passes `args` to the `Packager` if specified.
 
 For each (transitive) git dependency, the specified commit is checked out
 into a sub-directory of `packagesDir`. Already checked out dependencies are
@@ -122,10 +121,9 @@ def helpClean :=
 "Remove build outputs
 
 USAGE:
-  lake clean [-- <args>...]
+  lake clean
 
-Deletes the build directory of the package.
-Arguments to the  `Packager` itself can be specified with `args`."
+Deletes the build directory of the package."
 
 def helpScriptCli :=
 "Manage Lake scripts

Lake/CLI/Main.lean

@@ -33,11 +33,11 @@ structure LakeConfig where
   configFile : FilePath := defaultConfigFile
   leanInstall : LeanInstall
   lakeInstall : LakeInstall
-  args : List String := []
+  options : NameMap String := {}
 
 def loadPkg (config : LakeConfig) : LogIO Package := do
   setupLeanSearchPath config.leanInstall config.lakeInstall
-  Package.load config.rootDir config.args (config.rootDir / config.configFile)
+  Package.load config.rootDir config.options (config.rootDir / config.configFile)
 
 def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do
   if let Except.ok contents ← IO.FS.readFile manifestFile  |>.toBaseIO then
@@ -72,6 +72,7 @@ structure LakeOptions where
   configFile : FilePath := defaultConfigFile
   leanInstall? : Option LeanInstall := none
   lakeInstall? : Option LakeInstall := none
+  configOptions : NameMap String := {}
   subArgs : List String := []
   wantsHelp : Bool := false
 
@@ -111,12 +112,13 @@ def getInstall (opts : LakeOptions) : Except CliError (LeanInstall × LakeInstal
   return (← getLeanInstall opts, ← getLakeInstall opts)
 
 /-- Make a `LakeConfig` from a `LakeOptions`. -/
-def mkLakeConfig (opts : LakeOptions) (args : List String := []) : Except CliError LakeConfig := do
+def mkLakeConfig (opts : LakeOptions) : Except CliError LakeConfig := do
   let (leanInstall, lakeInstall) ← getInstall opts
   return {
     rootDir := opts.rootDir,
     configFile := opts.configFile,
-    leanInstall, lakeInstall, args
+    leanInstall, lakeInstall,
+    options := opts.configOptions
   }
 
 /-- Make a Lake `Context` from a `Workspace` and `LakeConfig`. -/
@@ -154,10 +156,21 @@ def noArgsRem (act : CliStateM α) : CliM α := do
 
 -- ## Option Parsing
 
+def setConfigOption (kvPair : String) : CliM PUnit :=
+  let pos := kvPair.posOf '='
+  let (key, val) :=
+    if pos = kvPair.endPos then
+      (kvPair.toName, "")
+    else
+      (kvPair.extract 0 pos |>.toName, kvPair.extract (kvPair.next pos) kvPair.endPos)
+  modifyThe LakeOptions fun opts =>
+    {opts with configOptions := opts.configOptions.insert key val}
+
 def shortOption : (opt : Char) → CliM PUnit
 | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
 | 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
 | 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
+| 'K' => do setConfigOption <| ← takeOptArg "-K" "key-value pair"
 | opt => throw <| CliError.unknownShortOption opt
 
 def longOption : (opt : String) → CliM PUnit
@@ -256,7 +269,7 @@ def script : (cmd : String) → CliM PUnit
         IO.println s!"{pkgName}/{scriptName}"
 | "run" => do
   processOptions lakeOption
-  let spec ← takeArg "script spec"; let args ← takeArgs
+  let spec ← takeArg "script name"; let args ← takeArgs
   let config ← mkLakeConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   let (pkg, scriptName) ← parseScriptSpec ws spec
@@ -270,7 +283,7 @@ def script : (cmd : String) → CliM PUnit
     throw <| CliError.unknownScript scriptName
 | "doc" => do
   processOptions lakeOption
-  let spec ← takeArg "script spec"
+  let spec ← takeArg "script name"
   let config ← mkLakeConfig (← getThe LakeOptions)
   noArgsRem do
     let ws ← loadWorkspace config
@@ -308,7 +321,7 @@ def command : (cmd : String) → CliM PUnit
 | "build" => do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let config ← mkLakeConfig opts opts.subArgs
+  let config ← mkLakeConfig opts
   let ws ← loadWorkspace config
   let targetSpecs ← takeArgs
   let target ← show Except _ _ from do
@@ -322,7 +335,7 @@ def command : (cmd : String) → CliM PUnit
 | "update" => do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let config ← mkLakeConfig opts opts.subArgs
+  let config ← mkLakeConfig opts
   noArgsRem <| discard <| loadWorkspace config (updateDeps := true)
 | "print-paths" => do
   processOptions lakeOption
@@ -331,7 +344,7 @@ def command : (cmd : String) → CliM PUnit
 | "clean" => do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let config ← mkLakeConfig opts opts.subArgs
+  let config ← mkLakeConfig opts
   noArgsRem <| (← loadPkg config).clean
 | "script" => do
   if let some cmd ← takeArg? then

Lake/Config/Dependency.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+import Lean.Data.Name
 
 namespace Lake
 open Lean System
@@ -17,7 +18,7 @@ In Lake, dependency sources currently come into flavors:
 -/
 inductive Source where
 | path (dir : FilePath)
-| git (url : String) (rev : Option String)
+| git (url : String) (rev : Option String) (subDir : Option FilePath)
 deriving Inhabited, Repr
 
 /-- A `Dependency` of a package. -/
@@ -33,13 +34,8 @@ structure Dependency where
   -/
   src  : Source
   /--
-  The subdirectory of the dependency's source where
-  the dependency's package configuration is located.
-  -/
-  dir  : FilePath := "."
-  /--
   Arguments to pass to the dependency's package configuration.
   -/
-  args : List String := []
+  options : NameMap String := {}
 
-deriving Inhabited, Repr
+deriving Inhabited

Lake/Config/Load.lean

@@ -38,10 +38,10 @@ def processHeader (header : Syntax) (opts : Options) (trustLevel : UInt32)
     modify (·.add { fileName := inputCtx.fileName, data := toString e, pos })
     mkEmptyEnvironment
 
-/-- Lake `Lean.Environment.evalConstCheck` but with plain universe-polymorphic `Except`. -/
+/-- Like `Lean.Environment.evalConstCheck` but with plain universe-polymorphic `Except`. -/
 unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (type : Name) (const : Name) : Except String α :=
   match env.find? const with
-  | none  => throw (s!"unknown constant '{const}'")
+  | none => throw s!"unknown constant '{const}'"
   | some info =>
     match info.type with
     | Expr.const c _ _ =>
@@ -57,7 +57,7 @@ where
 namespace Package
 
 /-- Unsafe implementation of `load`. -/
-unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
+unsafe def loadUnsafe (dir : FilePath) (configOpts : NameMap String)
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
 : LogIO Package := do
 
@@ -70,7 +70,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
 
   -- Configure Extensions
   let env := dirExt.setState env dir
-  let env := argsExt.setState env args
+  let env := optsExt.setState env configOpts
 
   -- Elaborate File
   let commandState := Elab.Command.mkState env messages leanOpts
@@ -81,82 +81,89 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
     | MessageSeverity.warning     => logWarning (← msg.toString)
     | MessageSeverity.error       => logError (← msg.toString)
 
-  -- Extract Configuration
+   -- Extract Configuration
+  if s.commandState.messages.hasErrors then
+    error s!"package configuration `{configFile}` has errors"
+
+  -- Load Package Configuration
   let env := s.commandState.env
-  if !s.commandState.messages.hasErrors then
+  let pkgDeclName ←
     match packageAttr.ext.getState env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
-    | [pkgDeclName] =>
-      -- Load Package Configuration
-      let config ← IO.ofExcept <| Id.run <| ExceptT.run <|
-        env.evalConstCheck PackageConfig leanOpts ``PackageConfig pkgDeclName
-      if config.extraDepTarget.isSome then
-        logWarning <| "`extraDepTarget` has been deprecated. " ++
-          "Try to use a custom target or raise an issue about your use case."
-      -- Tag Load Helpers
-      let mkTagMap {α} (attr) (f : Name → IO α) : IO (NameMap α) :=
-        attr.ext.getState env |>.foldM (init := {}) fun map declName =>
-          return map.insert declName <| ← f declName
-      let mkDTagMap {β} (attr : TagAttribute) (f : (n : WfName) → IO (β n)) : IO (DNameMap β) :=
-        attr.ext.getState env |>.foldM (init := {}) fun map declName =>
-          let declName := WfName.ofName declName
-          return map.insert declName <| ← f declName
-      let evalConst (α typeName declName) : IO α :=
-        IO.ofExcept (evalConstCheck α env leanOpts typeName declName)
-      let evalConstMap {α β} (f : α → β) (declName) : IO β :=
-        match env.evalConst α leanOpts declName with
-        | .ok a => pure <| f a
-        | .error e => throw <| IO.userError e
-       -- Load Target & Script Configurations
-      let scripts ← mkTagMap scriptAttr fun declName => do
-        let fn ← IO.ofExcept <| evalConstCheck ScriptFn env leanOpts ``ScriptFn declName
-        return {fn, doc? := (← findDocString? env declName)}
-      let leanLibConfigs ← mkTagMap leanLibAttr
-        (evalConst LeanLibConfig ``LeanLibConfig)
-      let leanExeConfigs ← mkTagMap leanExeAttr
-        (evalConst LeanExeConfig ``LeanExeConfig)
-      let externLibConfigs ← mkTagMap externLibAttr
-        (evalConst ExternLibConfig ``ExternLibConfig)
-      let opaqueModuleFacetConfigs ← mkDTagMap moduleFacetAttr fun name => do
-        match evalConstCheck ModuleFacetDecl env leanOpts ``ModuleFacetDecl name with
-        | .ok decl =>
-          if h : name = decl.name then
-            return OpaqueModuleFacetConfig.mk (h ▸ decl.config)
-          else
-            error s!"Facet was defined as `{decl.1}`, but was registered as `{name}`"
-        | .error e => throw <| IO.userError e
-      let opaquePackageFacetConfigs ← mkDTagMap packageFacetAttr fun name => do
-        match evalConstCheck PackageFacetDecl env leanOpts ``PackageFacetDecl name with
-        | .ok decl =>
-          if h : name = decl.name then
-            return OpaquePackageFacetConfig.mk (h ▸ decl.config)
-          else
-            error s!"Facet was defined as `{decl.1}`, but was registered as `{name}`"
-        | .error e => throw <| IO.userError e
-      let opaqueTargetConfigs ← mkTagMap targetAttr
-        (evalConstMap OpaqueTargetConfig.mk)
-      let defaultTargets :=
-        defaultTargetAttr.ext.getState env |>.fold (init := #[]) fun arr name =>
-          arr.push <| WfName.ofName name
-      -- Construct the Package
-      if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
-        logWarning <| "Package targets are deprecated. " ++
-          "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
-      return {
-        dir, config, scripts,
-        dependencies := depsExt.getState env,
-        leanLibConfigs, leanExeConfigs, externLibConfigs,
-        opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs,
-        defaultTargets
-      }
+    | [name] => pure name
     | _ => error s!"configuration file has multiple `package` declarations"
-  else
-    error s!"package configuration `{configFile}` has errors"
+  let config ← IO.ofExcept <|
+    evalConstCheck PackageConfig env leanOpts ``PackageConfig pkgDeclName
+  if config.extraDepTarget.isSome then
+    logWarning <| "`extraDepTarget` has been deprecated. " ++
+      "Try to use a custom target or raise an issue about your use case."
+
+  -- Tag Load Helpers
+  let mkTagMap {α} (attr) (f : Name → IO α) : IO (NameMap α) :=
+    attr.ext.getState env |>.foldM (init := {}) fun map declName =>
+      return map.insert declName <| ← f declName
+  let mkDTagMap {β} (attr : TagAttribute) (f : (n : WfName) → IO (β n)) : IO (DNameMap β) :=
+    attr.ext.getState env |>.foldM (init := {}) fun map declName =>
+      let declName := WfName.ofName declName
+      return map.insert declName <| ← f declName
+  let evalConst (α typeName declName) : IO α :=
+    IO.ofExcept (evalConstCheck α env leanOpts typeName declName)
+  let evalConstMap {α β} (f : α → β) (declName) : IO β :=
+    match env.evalConst α leanOpts declName with
+    | .ok a => pure <| f a
+    | .error e => throw <| IO.userError e
+
+  -- Load Dependency, Script, Facet, & Target Configurations
+  let dependencies ←
+    packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
+      return arr.push <| ← evalConst Dependency ``Dependency name
+  let scripts ← mkTagMap scriptAttr fun declName => do
+    let fn ← IO.ofExcept <| evalConstCheck ScriptFn env leanOpts ``ScriptFn declName
+    return {fn, doc? := (← findDocString? env declName)}
+  let leanLibConfigs ← mkTagMap leanLibAttr
+    (evalConst LeanLibConfig ``LeanLibConfig)
+  let leanExeConfigs ← mkTagMap leanExeAttr
+    (evalConst LeanExeConfig ``LeanExeConfig)
+  let externLibConfigs ← mkTagMap externLibAttr
+    (evalConst ExternLibConfig ``ExternLibConfig)
+  let opaqueModuleFacetConfigs ← mkDTagMap moduleFacetAttr fun name => do
+    match evalConstCheck ModuleFacetDecl env leanOpts ``ModuleFacetDecl name with
+    | .ok decl =>
+      if h : name = decl.name then
+        return OpaqueModuleFacetConfig.mk (h ▸ decl.config)
+      else
+        error s!"Facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .error e => throw <| IO.userError e
+  let opaquePackageFacetConfigs ← mkDTagMap packageFacetAttr fun name => do
+    match evalConstCheck PackageFacetDecl env leanOpts ``PackageFacetDecl name with
+    | .ok decl =>
+      if h : name = decl.name then
+        return OpaquePackageFacetConfig.mk (h ▸ decl.config)
+      else
+        error s!"Facet was defined as `{decl.name}`, but was registered as `{name}`"
+    | .error e => throw <| IO.userError e
+  let opaqueTargetConfigs ← mkTagMap targetAttr
+    (evalConstMap OpaqueTargetConfig.mk)
+  let defaultTargets :=
+    defaultTargetAttr.ext.getState env |>.fold (init := #[]) fun arr name =>
+      arr.push <| WfName.ofName name
+
+  -- Construct the Package
+  if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
+    logWarning <| "Package targets are deprecated. " ++
+      "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
+  return {
+    dir, config, scripts, dependencies,
+    leanLibConfigs, leanExeConfigs, externLibConfigs,
+    opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs,
+    defaultTargets
+  }
+
 
 /--
 Load the package located in
 the given directory with the given configuration file.
 -/
 @[implementedBy loadUnsafe]
-opaque load (dir : FilePath) (args : List String := [])
-(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package
+opaque load (dir : FilePath) (configOpts : NameMap String)
+(configFile := dir / defaultConfigFile) (leanOpts := Options.empty)  : LogIO Package