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.
This commit is contained in:
Mac Malone
GitHub
parent
cd4383b6f3
commit
cf2b7f4c1b
10 changed files with 178 additions and 130 deletions
|
|
@ -10,7 +10,7 @@ open Lean
|
|||
|
||||
namespace Lake
|
||||
|
||||
initialize
|
||||
builtin_initialize
|
||||
registerBuiltinAttribute {
|
||||
ref := by exact decl_name%
|
||||
name := `test_runner
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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]?)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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?
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue