diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean
index 9bcc07a7bf..ad9ef0e3e5 100644
--- a/src/lake/Lake/DSL/Attributes.lean
+++ b/src/lake/Lake/DSL/Attributes.lean
@@ -10,7 +10,7 @@ open Lean
 
 namespace Lake
 
-builtin_initialize
+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 083bba8601..89784b9eeb 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
 
-builtin_initialize packageAttr : OrderedTagAttribute ←
+initialize packageAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package "mark a definition as a Lake package configuration"
 
-builtin_initialize packageDepAttr : OrderedTagAttribute ←
+initialize packageDepAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
-builtin_initialize postUpdateAttr : OrderedTagAttribute ←
+initialize postUpdateAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
 
-builtin_initialize scriptAttr : OrderedTagAttribute ←
+initialize scriptAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `script "mark a definition as a Lake script"
 
-builtin_initialize defaultScriptAttr : OrderedTagAttribute ←
+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`"
 
-builtin_initialize leanLibAttr : OrderedTagAttribute ←
+initialize leanLibAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
 
-builtin_initialize leanExeAttr : OrderedTagAttribute ←
+initialize leanExeAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
 
-builtin_initialize externLibAttr : OrderedTagAttribute ←
+initialize externLibAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
 
-builtin_initialize targetAttr : OrderedTagAttribute ←
+initialize targetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `target "mark a definition as a custom Lake target"
 
-builtin_initialize defaultTargetAttr : OrderedTagAttribute ←
+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 @@ builtin_initialize defaultTargetAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
-builtin_initialize testDriverAttr : OrderedTagAttribute ←
+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 @@ builtin_initialize testDriverAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `test_driver` can only be used on a `script`, `lean_exe`, or `lean_lib`"
 
-builtin_initialize lintDriverAttr : OrderedTagAttribute ←
+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 @@ builtin_initialize lintDriverAttr : OrderedTagAttribute ←
       unless valid do
         throwError "attribute `lint_driver` can only be used on a `script` or `lean_exe`"
 
-builtin_initialize moduleFacetAttr : OrderedTagAttribute ←
+initialize moduleFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
 
-builtin_initialize packageFacetAttr : OrderedTagAttribute ←
+initialize packageFacetAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet"
 
-builtin_initialize libraryFacetAttr : OrderedTagAttribute ←
+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 766415a13f..20c9bd8ccb 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
 
-@[builtin_term_elab dirConst]
+@[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
 
-@[builtin_term_elab getConfig]
+@[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 b9fe936eba..150805a4f9 100644
--- a/src/lake/Lake/DSL/Extensions.lean
+++ b/src/lake/Lake/DSL/Extensions.lean
@@ -10,8 +10,8 @@ open Lean
 
 namespace Lake
 
-builtin_initialize dirExt : EnvExtension (Option System.FilePath) ←
+initialize dirExt : EnvExtension (Option System.FilePath) ←
   registerEnvExtension (pure none)
 
-builtin_initialize optsExt : EnvExtension (Option (NameMap String)) ←
+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 8b887f0196..b9e5a02c92 100644
--- a/src/lake/Lake/DSL/Meta.lean
+++ b/src/lake/Lake/DSL/Meta.lean
@@ -57,7 +57,7 @@ extern_lib linuxOnlyLib := ...
 scoped syntax (name := metaIf)
 "meta " "if " term " then " cmdDo (" else " cmdDo)? : command
 
-@[builtin_command_elab metaIf]
+@[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"
@@ -80,7 +80,7 @@ and produces an expression corresponding to the result via `ToExpr α`.
 -/
 scoped syntax:lead (name := runIO) "run_io " doSeq : term
 
-@[builtin_term_elab runIO]
+@[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 78d54e451a..12eff87777 100644
--- a/src/lake/Lake/DSL/Package.lean
+++ b/src/lake/Lake/DSL/Package.lean
@@ -34,7 +34,7 @@ The defined package configuration will be available for reference as `_package`.
 scoped syntax (name := packageDecl)
 (docComment)? (Term.attributes)? "package " structDeclSig : command
 
-@[builtin_command_elab packageDecl]
+@[command_elab packageDecl]
 def elabPackageDecl : CommandElab := fun stx => do
   let `(packageDecl|$(doc?)? $(attrs?)? package%$kw $sig) := stx
     | throwErrorAt stx "ill-formed package declaration"
@@ -74,7 +74,7 @@ scoped syntax (name := postUpdateDecl)
 optional(docComment) optional(Term.attributes)
 "post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command
 
-@[builtin_macro postUpdateDecl]
+@[macro postUpdateDecl]
 def expandPostUpdateDecl : Macro := fun stx => do
   match stx with
   | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>
diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean
index 684622d085..8d9b22fd5c 100644
--- a/src/lake/Lake/DSL/Require.lean
+++ b/src/lake/Lake/DSL/Require.lean
@@ -143,7 +143,7 @@ options to the dependency on the command line.
 scoped syntax (name := requireDecl)
 (docComment)? "require " depSpec : command
 
-@[builtin_macro requireDecl]
+@[macro requireDecl]
 def expandRequireDecl : Macro := fun stx => do
   let `(requireDecl|$(doc?)? require%$kw $spec) := stx
     | Macro.throwErrorAt stx "ill-formed require declaration"
diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean
index 05312de6be..9565f0cf88 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
 
-@[builtin_macro scriptDecl]
+@[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 513b54c567..7d10456348 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -44,7 +44,7 @@ The `mod` parameter (and its type specifier) is optional.
 scoped syntax (name := moduleFacetDecl)
 (docComment)? (Term.attributes)? "module_facet " buildDeclSig : command
 
-@[builtin_macro moduleFacetDecl]
+@[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"
@@ -83,7 +83,7 @@ The `pkg` parameter (and its type specifier) is optional.
 scoped syntax (name := packageFacetDecl)
 (docComment)? (Term.attributes)? "package_facet " buildDeclSig : command
 
-@[builtin_macro packageFacetDecl]
+@[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"
@@ -122,7 +122,7 @@ The `lib` parameter (and its type specifier) is optional.
 scoped syntax (name := libraryFacetDecl)
 (docComment)? (Term.attributes)? "library_facet " buildDeclSig : command
 
-@[builtin_macro libraryFacetDecl]
+@[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"
@@ -168,7 +168,7 @@ provided is the package in which the target is defined.
 scoped syntax (name := targetDecl)
 (docComment)? (Term.attributes)? "target " buildDeclSig : command
 
-@[builtin_macro targetDecl]
+@[macro targetDecl]
 def expandTargetDecl : Macro := fun stx => do
   let `(targetDecl|$(doc?)? $(attrs?)? target%$kw $sig) := stx
     | Macro.throwErrorAt stx "ill-formed target declaration"
@@ -203,7 +203,7 @@ lean_lib «target-name» where /- config opts -/
 scoped syntax (name := leanLibDecl)
 (docComment)? (Term.attributes)? "lean_lib " structDeclSig : command
 
-@[builtin_command_elab leanLibDecl]
+@[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"
@@ -231,7 +231,7 @@ lean_exe «target-name» where /- config opts -/
 scoped syntax (name := leanExeDecl)
 (docComment)? (Term.attributes)? "lean_exe " structDeclSig : command
 
-@[builtin_command_elab leanExeDecl]
+@[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"
@@ -274,7 +274,7 @@ The term should build the external library's **static** library.
 scoped syntax (name := externLibDecl)
 (docComment)? (Term.attributes)? "extern_lib " externLibDeclSpec : command
 
-@[builtin_macro externLibDecl]
+@[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"
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index 1aa88151ba..ac8e1e551a 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -250,7 +250,7 @@ private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr
 /-- A Lake version literal. -/
 scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
 
-@[builtin_term_elab verLit]
+@[term_elab verLit]
 def elabVerLit : TermElab := fun stx expectedType? => do
   let `(v!$v) := stx | throwUnsupportedSyntax
   tryPostponeIfNoneOrMVar expectedType?