From cf2b7f4c1bc43f75ff925e8acda8c748688c813a Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 26 Feb 2025 21:34:14 -0500 Subject: [PATCH] feat: lake: builtin inits, elabs, & macros for DSL (#7171) This PR changes the Lake DSL to use builtin elaborators, macros, and initializers. This works out of the box for the Lake executable and is supported in interactive contexts through the Lake plugin. --- src/lake/Lake/DSL/Attributes.lean | 2 +- src/lake/Lake/DSL/AttributesCore.lean | 30 ++-- src/lake/Lake/DSL/Config.lean | 4 +- src/lake/Lake/DSL/Extensions.lean | 4 +- src/lake/Lake/DSL/Meta.lean | 7 +- src/lake/Lake/DSL/Package.lean | 38 +++-- src/lake/Lake/DSL/Require.lean | 11 +- src/lake/Lake/DSL/Script.lean | 2 +- src/lake/Lake/DSL/Targets.lean | 207 +++++++++++++++----------- src/lake/Lake/Util/Version.lean | 3 +- 10 files changed, 178 insertions(+), 130 deletions(-) diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean index ad9ef0e3e5..9bcc07a7bf 100644 --- a/src/lake/Lake/DSL/Attributes.lean +++ b/src/lake/Lake/DSL/Attributes.lean @@ -10,7 +10,7 @@ open Lean namespace Lake -initialize +builtin_initialize registerBuiltinAttribute { ref := by exact decl_name% name := `test_runner diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean index 89784b9eeb..083bba8601 100644 --- a/src/lake/Lake/DSL/AttributesCore.lean +++ b/src/lake/Lake/DSL/AttributesCore.lean @@ -9,37 +9,37 @@ import Lake.Util.OrderedTagAttribute open Lean namespace Lake -initialize packageAttr : OrderedTagAttribute ← +builtin_initialize packageAttr : OrderedTagAttribute ← registerOrderedTagAttribute `package "mark a definition as a Lake package configuration" -initialize packageDepAttr : OrderedTagAttribute ← +builtin_initialize packageDepAttr : OrderedTagAttribute ← registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency" -initialize postUpdateAttr : OrderedTagAttribute ← +builtin_initialize postUpdateAttr : OrderedTagAttribute ← registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook" -initialize scriptAttr : OrderedTagAttribute ← +builtin_initialize scriptAttr : OrderedTagAttribute ← registerOrderedTagAttribute `script "mark a definition as a Lake script" -initialize defaultScriptAttr : OrderedTagAttribute ← +builtin_initialize defaultScriptAttr : OrderedTagAttribute ← registerOrderedTagAttribute `default_script "mark a Lake script as the package's default" fun name => do unless (← getEnv <&> (scriptAttr.hasTag · name)) do throwError "attribute `default_script` can only be used on a `script`" -initialize leanLibAttr : OrderedTagAttribute ← +builtin_initialize leanLibAttr : OrderedTagAttribute ← registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration" -initialize leanExeAttr : OrderedTagAttribute ← +builtin_initialize leanExeAttr : OrderedTagAttribute ← registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration" -initialize externLibAttr : OrderedTagAttribute ← +builtin_initialize externLibAttr : OrderedTagAttribute ← registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target" -initialize targetAttr : OrderedTagAttribute ← +builtin_initialize targetAttr : OrderedTagAttribute ← registerOrderedTagAttribute `target "mark a definition as a custom Lake target" -initialize defaultTargetAttr : OrderedTagAttribute ← +builtin_initialize defaultTargetAttr : OrderedTagAttribute ← registerOrderedTagAttribute `default_target "mark a Lake target as the package's default" fun name => do let valid ← getEnv <&> fun env => @@ -50,7 +50,7 @@ initialize defaultTargetAttr : OrderedTagAttribute ← unless valid do throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)" -initialize testDriverAttr : OrderedTagAttribute ← +builtin_initialize testDriverAttr : OrderedTagAttribute ← registerOrderedTagAttribute `test_driver "mark a Lake script, executable, or library as package's test driver" fun name => do let valid ← getEnv <&> fun env => @@ -60,7 +60,7 @@ initialize testDriverAttr : OrderedTagAttribute ← unless valid do throwError "attribute `test_driver` can only be used on a `script`, `lean_exe`, or `lean_lib`" -initialize lintDriverAttr : OrderedTagAttribute ← +builtin_initialize lintDriverAttr : OrderedTagAttribute ← registerOrderedTagAttribute `lint_driver "mark a Lake script or executable as package's linter" fun name => do let valid ← getEnv <&> fun env => @@ -69,11 +69,11 @@ initialize lintDriverAttr : OrderedTagAttribute ← unless valid do throwError "attribute `lint_driver` can only be used on a `script` or `lean_exe`" -initialize moduleFacetAttr : OrderedTagAttribute ← +builtin_initialize moduleFacetAttr : OrderedTagAttribute ← registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet" -initialize packageFacetAttr : OrderedTagAttribute ← +builtin_initialize packageFacetAttr : OrderedTagAttribute ← registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet" -initialize libraryFacetAttr : OrderedTagAttribute ← +builtin_initialize libraryFacetAttr : OrderedTagAttribute ← registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet" diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean index 20c9bd8ccb..766415a13f 100644 --- a/src/lake/Lake/DSL/Config.lean +++ b/src/lake/Lake/DSL/Config.lean @@ -28,7 +28,7 @@ during the Lakefile's elaboration. -/ scoped syntax (name := dirConst) "__dir__" : term -@[term_elab dirConst] +@[builtin_term_elab dirConst] def elabDirConst : TermElab := fun stx expectedType? => do let exp := if let some dir := dirExt.getState (← getEnv) then @@ -48,7 +48,7 @@ or via the `with` clause in a `require` statement. -/ scoped syntax (name := getConfig) "get_config? " ident :term -@[term_elab getConfig] +@[builtin_term_elab getConfig] def elabGetConfig : TermElab := fun stx expectedType? => do tryPostponeIfNoneOrMVar expectedType? match stx with diff --git a/src/lake/Lake/DSL/Extensions.lean b/src/lake/Lake/DSL/Extensions.lean index 150805a4f9..b9fe936eba 100644 --- a/src/lake/Lake/DSL/Extensions.lean +++ b/src/lake/Lake/DSL/Extensions.lean @@ -10,8 +10,8 @@ open Lean namespace Lake -initialize dirExt : EnvExtension (Option System.FilePath) ← +builtin_initialize dirExt : EnvExtension (Option System.FilePath) ← registerEnvExtension (pure none) -initialize optsExt : EnvExtension (Option (NameMap String)) ← +builtin_initialize optsExt : EnvExtension (Option (NameMap String)) ← registerEnvExtension (pure none) diff --git a/src/lake/Lake/DSL/Meta.lean b/src/lake/Lake/DSL/Meta.lean index 8251cf7bde..8b887f0196 100644 --- a/src/lake/Lake/DSL/Meta.lean +++ b/src/lake/Lake/DSL/Meta.lean @@ -57,7 +57,10 @@ extern_lib linuxOnlyLib := ... scoped syntax (name := metaIf) "meta " "if " term " then " cmdDo (" else " cmdDo)? : command -elab_rules : command | `(meta if $c then $t $[else $e?]?) => do +@[builtin_command_elab metaIf] +def elabMetaIf : CommandElab := fun stx => do + let `(meta if $c then $t $[else $e?]?) := stx + | throwErrorAt stx "ill-formed meta if command" if (← withRef c <| runTermElabM fun _ => evalTerm Bool (toTypeExpr Bool) c .unsafe) then let cmd := mkNullNode (expandCmdDo t) withMacroExpansion (← getRef) cmd <| elabCommand cmd @@ -77,7 +80,7 @@ and produces an expression corresponding to the result via `ToExpr α`. -/ scoped syntax:lead (name := runIO) "run_io " doSeq : term -@[term_elab runIO] +@[builtin_term_elab runIO] def elabRunIO : TermElab := fun stx expectedType? => match stx with | `(run_io%$tk $t) => withRef t do diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean index ac51c26fdf..78d54e451a 100644 --- a/src/lake/Lake/DSL/Package.lean +++ b/src/lake/Lake/DSL/Package.lean @@ -8,8 +8,9 @@ import Lake.Config.Package import Lake.DSL.Attributes import Lake.DSL.DeclUtil +open Lean Parser Elab Command + namespace Lake.DSL -open Lean Parser Command /-! # Package Declarations DSL definitions for packages and hooks. @@ -30,9 +31,14 @@ package «pkg-name» where /- config opts -/ There can only be one `package` declaration per Lake configuration file. The defined package configuration will be available for reference as `_package`. -/ -scoped elab (name := packageDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"package " sig:structDeclSig : command => withRef kw do +scoped syntax (name := packageDecl) +(docComment)? (Term.attributes)? "package " structDeclSig : command + +@[builtin_command_elab packageDecl] +def elabPackageDecl : CommandElab := fun stx => do + let `(packageDecl|$(doc?)? $(attrs?)? package%$kw $sig) := stx + | throwErrorAt stx "ill-formed package declaration" + withRef kw do let attr ← `(Term.attrInstance| «package») let attrs := #[attr] ++ expandAttrs attrs? elabConfigDecl ``PackageConfig sig doc? attrs packageDeclName @@ -42,7 +48,6 @@ abbrev PackageDecl := TSyntax ``packageDecl instance : Coe PackageDecl Command where coe x := ⟨x.raw⟩ - /-- Declare a post-`lake update` hook for the package. Runs the monadic action is after a successful `lake update` execution @@ -69,13 +74,16 @@ scoped syntax (name := postUpdateDecl) optional(docComment) optional(Term.attributes) "post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command -macro_rules -| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) => - `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?) -| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => withRef kw do - let pkg ← expandOptSimpleBinder pkg? - let pkgName := mkIdentFrom pkg `_package.name - let attr ← `(Term.attrInstance| «post_update») - let attrs := #[attr] ++ expandAttrs attrs? - `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl := - {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?) +@[builtin_macro postUpdateDecl] +def expandPostUpdateDecl : Macro := fun stx => do + match stx with + | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) => + `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?) + | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => withRef kw do + let pkg ← expandOptSimpleBinder pkg? + let pkgName := mkIdentFrom pkg `_package.name + let attr ← `(Term.attrInstance| «post_update») + let attrs := #[attr] ++ expandAttrs attrs? + `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl := + {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?) + | stx => Macro.throwErrorAt stx "ill-formed post_update declaration" diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean index 7fec264f74..684622d085 100644 --- a/src/lake/Lake/DSL/Require.lean +++ b/src/lake/Lake/DSL/Require.lean @@ -140,9 +140,14 @@ The `with` clause specifies a `NameMap String` of Lake options used to configure the dependency. This is equivalent to passing `-K` options to the dependency on the command line. -/ -scoped macro (name := requireDecl) -doc?:(docComment)? kw:"require " spec:depSpec : command => withRef kw do - expandDepSpec spec doc? +scoped syntax (name := requireDecl) +(docComment)? "require " depSpec : command + +@[builtin_macro requireDecl] +def expandRequireDecl : Macro := fun stx => do + let `(requireDecl|$(doc?)? require%$kw $spec) := stx + | Macro.throwErrorAt stx "ill-formed require declaration" + withRef kw do expandDepSpec spec doc? @[inherit_doc requireDecl] abbrev RequireDecl := TSyntax ``requireDecl diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean index 9565f0cf88..05312de6be 100644 --- a/src/lake/Lake/DSL/Script.lean +++ b/src/lake/Lake/DSL/Script.lean @@ -36,7 +36,7 @@ script «script-name» (args) do scoped syntax (name := scriptDecl) (docComment)? optional(Term.attributes) "script " scriptDeclSpec : command -@[macro scriptDecl] +@[builtin_macro scriptDecl] def expandScriptDecl : Macro | `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? do $seq $[$wds?:whereDecls]?) => do `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := do $seq $[$wds?:whereDecls]?) diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean index 5969951a36..513b54c567 100644 --- a/src/lake/Lake/DSL/Targets.lean +++ b/src/lake/Lake/DSL/Targets.lean @@ -11,9 +11,10 @@ import Lake.Build.Index Macros for declaring Lake targets and facets. -/ -namespace Lake.DSL -open Lean Parser Command open System (FilePath) +open Lean Parser Elab Command + +namespace Lake.DSL syntax buildDeclSig := identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple @@ -40,22 +41,26 @@ module_facet «facet-name» (mod : Module) : α := The `mod` parameter (and its type specifier) is optional. -/ -scoped macro (name := moduleFacetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"module_facet " sig:buildDeclSig : command => withRef kw do - match sig with - | `(buildDeclSig| $nameStx $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) => - let attr ← withRef kw `(Term.attrInstance| module_facet) - let attrs := #[attr] ++ expandAttrs attrs? - let id := expandIdentOrStrAsIdent nameStx - let facet := Name.quoteFrom id id.getId - let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet") - let mod ← expandOptSimpleBinder mod? - `(module_data $id : $ty - $[$doc?:docComment]? @[$attrs,*] abbrev $declId := - Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn) - $[$wds?:whereDecls]?) - | stx => Macro.throwErrorAt stx "ill-formed module facet declaration" +scoped syntax (name := moduleFacetDecl) +(docComment)? (Term.attributes)? "module_facet " buildDeclSig : command + +@[builtin_macro moduleFacetDecl] +def expandModuleFacetDecl : Macro := fun stx => do + let `(moduleFacetDecl|$(doc?)? $(attrs?)? module_facet%$kw $sig) := stx + | Macro.throwErrorAt stx "ill-formed module facet declaration" + let `(buildDeclSig| $nameStx $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) := sig + | Macro.throwErrorAt sig "ill-formed module facet declaration" + withRef kw do + let attr ← `(Term.attrInstance| «module_facet») + let attrs := #[attr] ++ expandAttrs attrs? + let id := expandIdentOrStrAsIdent nameStx + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet") + let mod ← expandOptSimpleBinder mod? + `(module_data $id : $ty + $[$doc?:docComment]? @[$attrs,*] abbrev $declId := + Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn) + $[$wds?:whereDecls]?) abbrev mkPackageFacetDecl (α) (facet : Name) @@ -75,22 +80,26 @@ package_facet «facet-name» (pkg : Package) : α := The `pkg` parameter (and its type specifier) is optional. -/ -scoped macro (name := packageFacetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"package_facet " sig:buildDeclSig : command => withRef kw do - match sig with - | `(buildDeclSig| $nameStx $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) => - let attr ← withRef kw `(Term.attrInstance| package_facet) - let attrs := #[attr] ++ expandAttrs attrs? - let id := expandIdentOrStrAsIdent nameStx - let facet := Name.quoteFrom id id.getId - let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet") - let pkg ← expandOptSimpleBinder pkg? - `(package_data $id : $ty - $[$doc?]? @[$attrs,*] abbrev $declId := - Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn) - $[$wds?:whereDecls]?) - | stx => Macro.throwErrorAt stx "ill-formed package facet declaration" +scoped syntax (name := packageFacetDecl) +(docComment)? (Term.attributes)? "package_facet " buildDeclSig : command + +@[builtin_macro packageFacetDecl] +def expandPackageFacetDecl : Macro := fun stx => do + let `(packageFacetDecl|$(doc?)? $(attrs?)? package_facet%$kw $sig) := stx + | Macro.throwErrorAt stx "ill-formed package facet declaration" + let `(buildDeclSig| $nameStx $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) := sig + | Macro.throwErrorAt sig "ill-formed package facet signature" + withRef kw do + let attr ← `(Term.attrInstance| «package_facet») + let attrs := #[attr] ++ expandAttrs attrs? + let id := expandIdentOrStrAsIdent nameStx + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet") + let pkg ← expandOptSimpleBinder pkg? + `(package_data $id : $ty + $[$doc?]? @[$attrs,*] abbrev $declId := + Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn) + $[$wds?:whereDecls]?) abbrev mkLibraryFacetDecl (α) (facet : Name) @@ -110,22 +119,27 @@ library_facet «facet-name» (lib : LeanLib) : α := The `lib` parameter (and its type specifier) is optional. -/ -scoped macro (name := libraryFacetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"library_facet " sig:buildDeclSig : command => withRef kw do - match sig with - | `(buildDeclSig| $nameStx $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) => - let attr ← withRef kw `(Term.attrInstance| library_facet) - let attrs := #[attr] ++ expandAttrs attrs? - let id := expandIdentOrStrAsIdent nameStx - let facet := Name.quoteFrom id id.getId - let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet") - let lib ← expandOptSimpleBinder lib? - `(library_data $id : $ty - $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl := - Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn) - $[$wds?:whereDecls]?) - | stx => Macro.throwErrorAt stx "ill-formed library facet declaration" +scoped syntax (name := libraryFacetDecl) +(docComment)? (Term.attributes)? "library_facet " buildDeclSig : command + +@[builtin_macro libraryFacetDecl] +def expandLibraryFacetDecl : Macro := fun stx => do + let `(libraryFacetDecl|$(doc?)? $(attrs?)? library_facet%$kw $sig) := stx + | Macro.throwErrorAt stx "ill-formed library facet declaration" + let `(buildDeclSig| $nameStx $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) := sig + | Macro.throwErrorAt sig "ill-formed library facet signature" + withRef kw do + let attr ← `(Term.attrInstance| «library_facet») + let attrs := #[attr] ++ expandAttrs attrs? + let id := expandIdentOrStrAsIdent nameStx + let facet := Name.quoteFrom id id.getId + let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet") + let lib ← expandOptSimpleBinder lib? + `(library_data $id : $ty + $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl := + Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn) + $[$wds?:whereDecls]?) + -------------------------------------------------------------------------------- /-! ## Custom Target Declaration -/ @@ -151,22 +165,25 @@ The `pkg` parameter (and its type specifier) is optional. It is of type `NPackage _package.name` to provably demonstrate the package provided is the package in which the target is defined. -/ -scoped macro (name := targetDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"target " sig:buildDeclSig : command => do - match sig with - | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) => - let attr ← withRef kw `(Term.attrInstance| target) - let attrs := #[attr] ++ expandAttrs attrs? - let name := Name.quoteFrom id id.getId - let pkgName := mkIdentFrom id `_package.name - let pkg ← expandOptSimpleBinder pkg? - `(family_def $id : CustomData ($pkgName, $name) := $ty - $[$doc?]? @[$attrs,*] abbrev $id := - Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn) - $[$wds?:whereDecls]?) - | stx => Macro.throwErrorAt stx "ill-formed target declaration" +scoped syntax (name := targetDecl) +(docComment)? (Term.attributes)? "target " buildDeclSig : command +@[builtin_macro targetDecl] +def expandTargetDecl : Macro := fun stx => do + let `(targetDecl|$(doc?)? $(attrs?)? target%$kw $sig) := stx + | Macro.throwErrorAt stx "ill-formed target declaration" + let `(buildDeclSig|$id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) := sig + | Macro.throwErrorAt sig "ill-formed target signature" + withRef kw do + let attr ← `(Term.attrInstance| «target») + let attrs := #[attr] ++ expandAttrs attrs? + let name := Name.quoteFrom id id.getId + let pkgName := mkIdentFrom id `_package.name + let pkg ← expandOptSimpleBinder pkg? + `(family_def $id : CustomData ($pkgName, $name) := $ty + $[$doc?]? @[$attrs,*] abbrev $id := + Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn) + $[$wds?:whereDecls]?) -------------------------------------------------------------------------------- /-! ## Lean Library & Executable Target Declarations -/ @@ -183,10 +200,15 @@ lean_lib «target-name» { /- config opts -/ } lean_lib «target-name» where /- config opts -/ ``` -/ -scoped elab (name := leanLibDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"lean_lib " sig:structDeclSig : command => withRef kw do - let attr ← `(Term.attrInstance| lean_lib) +scoped syntax (name := leanLibDecl) +(docComment)? (Term.attributes)? "lean_lib " structDeclSig : command + +@[builtin_command_elab leanLibDecl] +def elabLeanLibDecl : CommandElab := fun stx => do + let `(leanLibDecl|$(doc?)? $(attrs?)? lean_lib%$kw $sig) := stx + | throwErrorAt stx "ill-formed lean_lib declaration" + withRef kw do + let attr ← `(Term.attrInstance| «lean_lib») let attrs := #[attr] ++ expandAttrs attrs? elabConfigDecl ``LeanLibConfig sig doc? attrs @@ -206,10 +228,15 @@ lean_exe «target-name» { /- config opts -/ } lean_exe «target-name» where /- config opts -/ ``` -/ -scoped elab (name := leanExeDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"lean_exe " sig:structDeclSig : command => withRef kw do - let attr ← `(Term.attrInstance| lean_exe) +scoped syntax (name := leanExeDecl) +(docComment)? (Term.attributes)? "lean_exe " structDeclSig : command + +@[builtin_command_elab leanExeDecl] +def elabLeanExeDecl : CommandElab := fun stx => do + let `(leanExeDecl|$(doc?)? $(attrs?)? lean_exe%$kw $sig) := stx + | throwErrorAt stx "ill-formed lean_exe declaration" + withRef kw do + let attr ← `(Term.attrInstance| «lean_exe») let attrs := #[attr] ++ expandAttrs attrs? elabConfigDecl ``LeanExeConfig sig doc? attrs @@ -244,18 +271,22 @@ provided is the package in which the target is defined. The term should build the external library's **static** library. -/ -scoped macro (name := externLibDecl) -doc?:optional(docComment) attrs?:optional(Term.attributes) -kw:"extern_lib " spec:externLibDeclSpec : command => withRef kw do - match spec with - | `(externLibDeclSpec| $nameStx $[$pkg?]? := $defn $[$wds?:whereDecls]?) => - let attr ← `(Term.attrInstance| extern_lib) - let attrs := #[attr] ++ expandAttrs attrs? - let id := expandIdentOrStrAsIdent nameStx - let pkgName := mkIdentFrom id `_package.name - let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static) - let name := Name.quoteFrom id id.getId - `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]? - $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := - Lake.DSL.mkExternLibDecl $pkgName $name) - | stx => Macro.throwErrorAt stx "ill-formed external library declaration" +scoped syntax (name := externLibDecl) +(docComment)? (Term.attributes)? "extern_lib " externLibDeclSpec : command + +@[builtin_macro externLibDecl] +def expandExternLibDecl : Macro := fun stx => do + let `(externLibDecl|$(doc?)? $(attrs?)? extern_lib%$kw $spec) := stx + | Macro.throwErrorAt stx "ill-formed external library declaration" + let `(externLibDeclSpec| $nameStx $[$pkg?]? := $defn $[$wds?:whereDecls]?) := spec + | Macro.throwErrorAt spec "ill-formed external library signature" + withRef kw do + let attr ← `(Term.attrInstance| «extern_lib») + let attrs := #[attr] ++ expandAttrs attrs? + let id := expandIdentOrStrAsIdent nameStx + let pkgName := mkIdentFrom id `_package.name + let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static) + let name := Name.quoteFrom id id.getId + `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]? + $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := + Lake.DSL.mkExternLibDecl $pkgName $name) diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index fdf0d12a5f..1aa88151ba 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -250,7 +250,8 @@ private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr /-- A Lake version literal. -/ scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term -@[term_elab verLit] def elabVerLit : TermElab := fun stx expectedType? => do +@[builtin_term_elab verLit] +def elabVerLit : TermElab := fun stx expectedType? => do let `(v!$v) := stx | throwUnsupportedSyntax tryPostponeIfNoneOrMVar expectedType? let some expectedType := expectedType?