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?