feat: replace __args__ with get_config? + related refactors

2022-07-08 19:00:52 -04:00 · 2022-07-08 19:00:52 -04:00 · 0fbd7a866a
commit 0fbd7a866a
parent 185e10f6f3
12 changed files with 175 additions and 167 deletions
--- a/Lake/CLI/Help.lean
+++ b/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
--- a/Lake/CLI/Main.lean
+++ b/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
--- a/Lake/Config/Dependency.lean
+++ b/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
--- a/Lake/Config/Load.lean
+++ b/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
--- a/Lake/Config/Resolve.lean
+++ b/Lake/Config/Resolve.lean
@ -81,11 +81,11 @@ def materializeDep (ws : Workspace)
 (pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM FilePath :=
  match dep.src with
  | Source.path dir => return pkg.dir / dir
-  | Source.git url rev? => do
+  | Source.git url rev? subDir? => do
    let name := dep.name.toString (escape := false)
-    let depDir := ws.packagesDir / name
-    materializeGitPkg name depDir url rev? shouldUpdate
-    return depDir
+    let gitDir := ws.packagesDir / name
+    materializeGitPkg name gitDir url rev? shouldUpdate
+    return match subDir? with | some subDir => gitDir / subDir | none => gitDir

 /--
 Resolves a `Dependency` relative to the given `Package`
@ -94,7 +94,7 @@ in the same `Workspace`, downloading and/or updating it as necessary.
 def resolveDep (ws : Workspace)
 (pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM Package := do
  let dir ← materializeDep ws pkg dep shouldUpdate
-  let depPkg ← Package.load (dir / dep.dir) dep.args
+  let depPkg ← Package.load dir dep.options
  unless depPkg.name == dep.name do
    throw <| IO.userError <|
      s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
@ -11,6 +11,9 @@ namespace Lake
 initialize packageAttr : TagAttribute ←
  registerTagAttribute `package "mark a definition as a Lake package configuration"

+initialize packageDepAttr : TagAttribute ←
+  registerTagAttribute `packageDep "mark a definition as a Lake package dependency"
+
 initialize scriptAttr : TagAttribute ←
  registerTagAttribute `script "mark a definition as a Lake script"

--- a/Lake/DSL/Config.lean
+++ b/Lake/DSL/Config.lean
@ -16,10 +16,10 @@ outside Lakefile elaboration (e.g., when editing).
 opaque dummyDir : System.FilePath

 /--
-A dummy default constant for `__args__` to make it type check
+A dummy default constant for `get_config` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
-opaque dummyArgs : List String
+opaque dummyGetConfig? : Name → Option String

 /--
 A macro that expands to the path of package's directory
@ -39,17 +39,22 @@ def elabDirConst : TermElab := fun stx expectedType? => do
  withMacroExpansion stx exp <| elabTerm exp expectedType?

 /--
-A macro that expands to the configuration arguments passed
-via the Lake command line during the Lakefile's elaboration.
-/
-scoped syntax (name := argsConst) "__args__" :term
+A macro that expands to the specified configuration option (or `none`,
+if not the option has not been set) during the Lakefile's elaboration.

-@[termElab argsConst]
-def elabArgsConst : TermElab := fun stx expectedType? => do
-  let exp :=
-    if let some args := argsExt.getState (← getEnv) then
-      quote (k := `term) args
-    else
-      -- `id` app forces Lean to show macro's doc rather than the constant's
-      Syntax.mkApp (mkCIdentFrom stx ``id) #[mkCIdentFrom stx ``dummyArgs]
-  withMacroExpansion stx exp <| elabTerm exp expectedType?
+Configuration arguments are set either via the Lake CLI (by the `-K` option)
+or via the `with` clause in a `require` statement.
+-/
+scoped syntax (name := getConfig) "get_config? " ident :term
+
+@[termElab getConfig]
+def elabGetConfig : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(getConfig| get_config? $key) =>
+    let exp :=
+      if let some opts := optsExt.getState (← getEnv) then
+        quote (k := `term) <| opts.find? key.getId
+      else
+        Syntax.mkApp (mkCIdentFrom stx ``dummyGetConfig?) #[quote key.getId]
+    withMacroExpansion stx exp <| elabTerm exp expectedType?
+  | _ => throwUnsupportedSyntax
--- a/Lake/DSL/Extensions.lean
+++ b/Lake/DSL/Extensions.lean
@ -10,11 +10,8 @@ open Lean

 namespace Lake

-initialize depsExt : EnvExtension (Array Dependency) ←
-  registerEnvExtension (pure #[])
-
 initialize dirExt : EnvExtension (Option System.FilePath) ←
  registerEnvExtension (pure none)

-initialize argsExt : EnvExtension (Option (List String)) ←
+initialize optsExt : EnvExtension (Option (NameMap String)) ←
  registerEnvExtension (pure none)
--- a/Lake/DSL/Require.lean
+++ b/Lake/DSL/Require.lean
@ -3,12 +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 Lean.Elab.Command
-import Lake.Util.EvalTerm
+import Lean.Parser.Command
 import Lake.DSL.Extensions

 namespace Lake.DSL
-open Lean Meta Elab Command
+open Lean Parser Command

 syntax fromPath :=
  term
@ -16,34 +15,27 @@ syntax fromPath :=
 syntax fromGit :=
  &" git " term:max ("@" term:max)? ("/" term)?

-syntax fromClause :=
-  fromGit <|> fromPath
-
 syntax depSpec :=
-  ident " from " fromClause (" with " term)?
+  ident " from " (fromGit <|> fromPath) (" with " term)?

-def evalDepSpec : Syntax → TermElabM Dependency
-| `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $args?:term]?) => do
-  let url ← evalTerm String url
-  let rev ←
-    match rev? with
-    | some rev => some <$> evalTerm String rev
-    | none => pure none
-  let path ←
-    match path? with
-    | some path => evalTerm System.FilePath path
-    | none => pure "."
-  let args ← match args? with
-    | some args => evalTerm (List String) args
-    | none => pure []
-  return {name := name.getId, src := Source.git url rev, dir := path, args}
-| `(depSpec| $name:ident from $path:term $[with $args?:term]?) => do
-  let path ← evalTerm System.FilePath path
-  let args ← match args? with
-    | some args => evalTerm (List String) args
-    | none => pure []
-  return {name := name.getId, src := Source.path path, args}
-| _ => throwUnsupportedSyntax
+def expandDepSpec : TSyntax ``depSpec → MacroM Command
+| `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $opts?]?) => do
+  let rev ← match rev? with | some rev => `(some $rev) | none => `(none)
+  let path ← match path? with | some path => `(some $path) | none => `(none)
+  let opts := opts?.getD <| ← `({})
+  `(@[packageDep] def $name : Dependency := {
+    name := $(quote name.getId),
+    src := Source.git $url $rev $path,
+    options := $opts
+  })
+| `(depSpec| $name:ident from $path:term $[with $opts?]?) => do
+  let opts := opts?.getD <| ← `({})
+  `(@[packageDep] def $name : Dependency := {
+    name :=  $(quote name.getId),
+    src := Source.path $path,
+    options := $opts
+  })
+| _ => Macro.throwUnsupported

 /--
 Adds a mew package dependency to the workspace. Has two forms:
@ -61,6 +53,5 @@ The elements of both the `from` and `with` clauses are proper terms so
 normal computation is supported within them (though parentheses made be
 required to disambiguate the syntax).
 -/
-scoped elab (name := requireDecl) "require " spec:depSpec : command => do
-  let dep ← runTermElabM none <| fun _ => evalDepSpec spec
-  modifyEnv (depsExt.modifyState · (·.push dep))
+scoped macro (name := requireDecl) "require " spec:depSpec : command =>
+  expandDepSpec spec
--- a/Lake/Util/Cli.lean
+++ b/Lake/Util/Cli.lean
@ -77,22 +77,20 @@ variable [Monad m] [MonadStateOf ArgList m]
 /-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/
@[inline] def longOptionOrSpace (handle : String → m α) (opt : String) : m α :=
  let pos := opt.posOf ' '
-  let arg := opt.drop pos.byteIdx.succ -- TODO: this code is only correct if all characters in `opt` have size 1
-  if arg.isEmpty then
+  if pos = opt.endPos then
    handle opt
  else do
-    consArg arg
-    handle <| opt.take pos.byteIdx |>.trimLeft -- TODO: this code is only correct if all characters in `opt` have size 1
+    consArg <| opt.extract (opt.next pos) opt.endPos
+    handle <| opt.extract 0 pos

 /-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
@[inline] def longOptionOrEq (handle : String → m α) (opt : String) : m α :=
  let pos := opt.posOf '='
-  let arg := opt.drop pos.byteIdx.succ -- TODO: this code is only correct if all characters in `opt` have size 1
-  if arg.isEmpty then
+  if pos = opt.endPos then
    handle opt
  else do
-    consArg arg
-    handle <| opt.take pos.byteIdx -- TODO: this code is only correct if all characters in `opt` have size 1
+    consArg <| opt.extract (opt.next pos) opt.endPos
+    handle <| opt.extract 0 pos

 /-- Process a long option  of the form `--long`, `--long=arg`, `"--long arg"`. -/
@[inline] def longOption (handle : String → m α) : String → m α :=
--- a/test/50/foo/lakefile.lean
+++ b/test/50/foo/lakefile.lean
@ -2,8 +2,8 @@ import Lake
 open Lake DSL

 package foo where
-  moreLeanArgs := #[(__args__).get! 0]
-  moreLeancArgs := #[(__args__).get! 1]
+  moreLeanArgs := get_config? leanArgs |>.getD "" |>.splitOn " " |>.toArray
+  moreLeancArgs := get_config? leancArgs |>.getD "" |>.splitOn " " |>.toArray

@[defaultTarget]
 lean_exe foo
--- a/test/50/test.sh
+++ b/test/50/test.sh
@ -5,7 +5,7 @@ LAKE=${LAKE:-../../../build/bin/lake}

 cd foo
 rm -rf build
-${LAKE} build -- -Dhygiene=true -DBAR | grep -m2 foo.c
-${LAKE} build -- -Dhygiene=false -DBAZ | grep -m2 foo.c
-${LAKE} build -- -Dhygiene=false -DBAR | grep -m1 foo.o
-${LAKE} build -- -Dhygiene=true -DBAR | grep -m1 foo.olean
+${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m2 foo.c
+${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAZ | grep -m2 foo.c
+${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAR | grep -m1 foo.o
+${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m1 foo.olean