From 7e9014ed4075122ce748d8c13191f64242f4f6ca Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 8 Jul 2022 19:00:52 -0400 Subject: [PATCH] feat: replace `__args__` with `get_config?` + related refactors --- Lake/CLI/Help.lean | 12 ++- Lake/CLI/Main.lean | 31 +++++--- Lake/Config/Dependency.lean | 12 +-- Lake/Config/Load.lean | 153 +++++++++++++++++++----------------- Lake/Config/Resolve.lean | 10 +-- Lake/DSL/Attributes.lean | 3 + Lake/DSL/Config.lean | 33 ++++---- Lake/DSL/Extensions.lean | 5 +- Lake/DSL/Require.lean | 57 ++++++-------- Lake/Util/Cli.lean | 14 ++-- test/50/foo/lakefile.lean | 4 +- test/50/test.sh | 8 +- 12 files changed, 175 insertions(+), 167 deletions(-) diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean index 7b88306..289ddfc 100644 --- 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 [] create a Lean package in a new directory @@ -60,7 +61,7 @@ def helpBuild := "Build targets USAGE: - lake build [...] [-- ...] + lake build [...] 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 [-- ...] + 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 [-- ...] + 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 diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index ce59518..4b366ff 100644 --- 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 diff --git a/Lake/Config/Dependency.lean b/Lake/Config/Dependency.lean index b6226ef..4553132 100644 --- 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 diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index b4d7d38..af8a25b 100644 --- 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 diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean index bc12c8c..dcd87f3 100644 --- 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}, " ++ diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean index 1135ebf..998028a 100644 --- 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" diff --git a/Lake/DSL/Config.lean b/Lake/DSL/Config.lean index 811b6ef..25e8275 100644 --- 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. +A macro that expands to the specified configuration option (or `none`, +if not the option has not been set) during the Lakefile's elaboration. + +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 := argsConst) "__args__" :term +scoped syntax (name := getConfig) "get_config? " ident :term -@[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? +@[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 diff --git a/Lake/DSL/Extensions.lean b/Lake/DSL/Extensions.lean index f1ab0cf..9bdacff 100644 --- 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) diff --git a/Lake/DSL/Require.lean b/Lake/DSL/Require.lean index aedabd4..72bbf53 100644 --- 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)? - -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 + ident " from " (fromGit <|> fromPath) (" with " term)? + +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 diff --git a/Lake/Util/Cli.lean b/Lake/Util/Cli.lean index d529880..cf683c0 100644 --- 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 α := diff --git a/test/50/foo/lakefile.lean b/test/50/foo/lakefile.lean index 2e6565d..9138379 100644 --- 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 diff --git a/test/50/test.sh b/test/50/test.sh index d8a2fdf..157f314 100755 --- 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