diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 778bc415e8..5724bef0d5 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -22,7 +22,7 @@ namespace Lake
 Converts a conveniently typed target facet build function into its
 dynamically typed equivalent.
 -/
-@[macroInline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
+@[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
 [h : FamilyDef TargetData facet α] : IndexBuildM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
@@ -81,7 +81,7 @@ def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
 Recursively build the given info using the Lake build index
 and a topological / suspending scheduler and return the dynamic result.
 -/
-@[macroInline] def buildIndexTop (info : BuildInfo)
+@[macro_inline] def buildIndexTop (info : BuildInfo)
 [FamilyDef BuildData info.key α] : RecBuildM α := do
   cast (by simp) <| buildIndexTop' info
 
diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean
index 763f6cb1fb..4c6dab44d7 100644
--- a/Lake/CLI/Init.lean
+++ b/Lake/CLI/Init.lean
@@ -55,7 +55,7 @@ lean_lib {root} \{
   -- add library configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_exe {pkgName} \{
   root := `Main
 }
@@ -69,7 +69,7 @@ package {pkgName} \{
   -- add package configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_exe {exeRoot} \{
   -- add executable configuration options here
 }
@@ -83,7 +83,7 @@ package {pkgName} \{
   -- add package configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_lib {libRoot} \{
   -- add library configuration options here
 }
@@ -100,7 +100,7 @@ package {pkgName} \{
 require mathlib from git
   \"https://github.com/leanprover-community/mathlib4.git\"
 
-@[defaultTarget]
+@[default_target]
 lean_lib {libRoot} \{
   -- add any library configuration options here
 }
diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean
index c930bc77ec..f8552d5dc6 100644
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
@@ -12,25 +12,25 @@ 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"
+  registerTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
 initialize scriptAttr : TagAttribute ←
   registerTagAttribute `script "mark a definition as a Lake script"
 
 initialize leanLibAttr : TagAttribute ←
-  registerTagAttribute `leanLib "mark a definition as a Lake Lean library target configuration"
+  registerTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
 
 initialize leanExeAttr : TagAttribute ←
-  registerTagAttribute `leanExe "mark a definition as a Lake Lean executable target configuration"
+  registerTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
 
 initialize externLibAttr : TagAttribute ←
-  registerTagAttribute `externLib "mark a definition as a Lake external library target"
+  registerTagAttribute `extern_lib "mark a definition as a Lake external library target"
 
 initialize targetAttr : TagAttribute ←
   registerTagAttribute `target "mark a definition as a custom Lake target"
 
 initialize defaultTargetAttr : TagAttribute ←
-  registerTagAttribute `defaultTarget "mark a Lake target as the package's default"
+  registerTagAttribute `default_target "mark a Lake target as the package's default"
     fun name => do
       let valid ← getEnv <&> fun env =>
         leanLibAttr.hasTag env name ||
@@ -38,13 +38,13 @@ initialize defaultTargetAttr : TagAttribute ←
         externLibAttr.hasTag env name ||
         targetAttr.hasTag env name
       unless valid do
-        throwError "attribute `defaultTarget` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
+        throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
 
 initialize moduleFacetAttr : TagAttribute ←
-  registerTagAttribute `moduleFacet "mark a definition as a Lake module facet"
+  registerTagAttribute `module_facet "mark a definition as a Lake module facet"
 
 initialize packageFacetAttr : TagAttribute ←
-  registerTagAttribute `packageFacet "mark a definition as a Lake package facet"
+  registerTagAttribute `package_facet "mark a definition as a Lake package facet"
 
 initialize libraryFacetAttr : TagAttribute ←
-  registerTagAttribute `libraryFacet "mark a definition as a Lake library facet"
+  registerTagAttribute `library_facet "mark a definition as a Lake library facet"
diff --git a/Lake/DSL/Config.lean b/Lake/DSL/Config.lean
index 28b7112f18..05c09499ec 100644
--- a/Lake/DSL/Config.lean
+++ b/Lake/DSL/Config.lean
@@ -27,7 +27,7 @@ during the Lakefile's elaboration.
 -/
 scoped syntax (name := dirConst) "__dir__" : term
 
-@[termElab dirConst]
+@[term_elab dirConst]
 def elabDirConst : TermElab := fun stx expectedType? => do
   let exp :=
     if let some dir := dirExt.getState (← getEnv) then
@@ -47,7 +47,7 @@ or via the `with` clause in a `require` statement.
 -/
 scoped syntax (name := getConfig) "get_config? " ident :term
 
-@[termElab getConfig]
+@[term_elab getConfig]
 def elabGetConfig : TermElab := fun stx expectedType? => do
   tryPostponeIfNoneOrMVar expectedType?
   match stx with
diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean
index 23558e37ca..43f5d23bcb 100644
--- a/Lake/DSL/Facets.lean
+++ b/Lake/DSL/Facets.lean
@@ -34,7 +34,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"module_facet " sig:buildDeclSig : command => do
   match sig with
   | `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?]?) =>
-    let attr ← withRef kw `(Term.attrInstance| moduleFacet)
+    let attr ← withRef kw `(Term.attrInstance| module_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
@@ -63,7 +63,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"package_facet " sig:buildDeclSig : command => do
   match sig with
   | `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
-    let attr ← withRef kw `(Term.attrInstance| packageFacet)
+    let attr ← withRef kw `(Term.attrInstance| package_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
@@ -92,7 +92,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
 kw:"library_facet " sig:buildDeclSig : command => do
   match sig with
   | `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?]?) =>
-    let attr ← withRef kw `(Term.attrInstance| libraryFacet)
+    let attr ← withRef kw `(Term.attrInstance| library_facet)
     let attrs := #[attr] ++ expandAttrs attrs?
     let name := Name.quoteFrom id id.getId
     let facetId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
@@ -159,7 +159,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
 "extern_lib " spec:externLibDeclSpec : command => do
   match spec with
   | `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?]?) =>
-    let attr ← `(Term.attrInstance| externLib)
+    let attr ← `(Term.attrInstance| extern_lib)
     let attrs := #[attr] ++ expandAttrs attrs?
     let pkgName := mkIdentFrom id `_package.name
     let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
diff --git a/Lake/DSL/Require.lean b/Lake/DSL/Require.lean
index e68e6128e0..78df0cd748 100644
--- a/Lake/DSL/Require.lean
+++ b/Lake/DSL/Require.lean
@@ -23,14 +23,14 @@ def expandDepSpec : TSyntax ``depSpec → MacroM Command
   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 := {
+  `(@[package_dep] 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 := {
+  `(@[package_dep] def $name : Dependency := {
     name :=  $(quote name.getId),
     src := Source.path $path,
     options := $opts
diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean
index d834857240..56c223ab00 100644
--- a/Lake/DSL/Targets.lean
+++ b/Lake/DSL/Targets.lean
@@ -31,7 +31,7 @@ lean_lib «target-name» := /- config -/
 scoped macro (name := leanLibDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 "lean_lib " sig:structDeclSig : command => do
-  let attr ← `(Term.attrInstance| leanLib)
+  let attr ← `(Term.attrInstance| lean_lib)
   let ty := mkCIdentFrom (← getRef) ``LeanLibConfig
   let attrs := #[attr] ++ expandAttrs attrs?
   mkConfigStructDecl none doc? attrs ty sig
@@ -51,7 +51,7 @@ lean_exe «target-name» := /- config -/
 scoped macro (name := leanExeDecl)
 doc?:optional(docComment) attrs?:optional(Term.attributes)
 "lean_exe " sig:structDeclSig : command => do
-  let attr ← `(Term.attrInstance| leanExe)
+  let attr ← `(Term.attrInstance| lean_exe)
   let ty := mkCIdentFrom (← getRef) ``LeanExeConfig
   let attrs := #[attr] ++ expandAttrs attrs?
   mkConfigStructDecl none doc? attrs ty sig
diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean
index d495a8bcea..53ff7a8575 100644
--- a/Lake/Load/Package.lean
+++ b/Lake/Load/Package.lean
@@ -31,7 +31,7 @@ where
     throw s!"unexpected type at '{const}', `{type}` expected"
 
 /-- Like `Lean.Environment.evalConstCheck`, but with plain universe-polymorphic `Except`. -/
-@[implementedBy unsafeEvalConstCheck] opaque evalConstCheck
+@[implemented_by unsafeEvalConstCheck] opaque evalConstCheck
 (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α
 
 /-- Construct a `NameMap` from the declarations tagged with `attr`. -/
diff --git a/Lake/Util/Binder.lean b/Lake/Util/Binder.lean
index b95e4b758c..21adec6e6a 100644
--- a/Lake/Util/Binder.lean
+++ b/Lake/Util/Binder.lean
@@ -45,7 +45,7 @@ abbrev FunBinder := TSyntax ``Term.funBinder
 instance : Coe BinderIdent FunBinder where
   coe s := ⟨s.raw⟩
 
-@[runParserAttributeHooks]
+@[run_parser_attribute_hooks]
 def binder := Term.binderIdent <|> Term.bracketedBinder
 
 abbrev Binder := TSyntax ``binder
diff --git a/Lake/Util/Compare.lean b/Lake/Util/Compare.lean
index 80a2a880c9..a125964442 100644
--- a/Lake/Util/Compare.lean
+++ b/Lake/Util/Compare.lean
@@ -88,7 +88,7 @@ instance : LawfulCmpEq String compare where
   eq_of_cmp := eq_of_compareOfLessAndEq
   cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _
 
-@[macroInline]
+@[macro_inline]
 def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering
 | none,   none    => .eq
 | none,   some _  => .lt
diff --git a/Lake/Util/EvalTerm.lean b/Lake/Util/EvalTerm.lean
index 3d84eac397..603f2ea546 100644
--- a/Lake/Util/EvalTerm.lean
+++ b/Lake/Util/EvalTerm.lean
@@ -11,7 +11,7 @@ open Lean Elab
 unsafe def unsafeEvalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α := do
   Term.evalTerm α (toTypeExpr α) term .unsafe
 
-@[implementedBy unsafeEvalTerm]
+@[implemented_by unsafeEvalTerm]
 opaque evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
 
 /-! ## ToExpr Instances -/
diff --git a/Lake/Util/Family.lean b/Lake/Util/Family.lean
index 1ebeb83aa8..7d08bb9816 100644
--- a/Lake/Util/Family.lean
+++ b/Lake/Util/Family.lean
@@ -143,11 +143,11 @@ export FamilyDef (family_key_eq_type)
 attribute [simp] family_key_eq_type
 
 /-- Cast a datum from its individual type to its general family. -/
-@[macroInline] def toFamily [FamilyDef Fam a β] (b : β) : Fam a :=
+@[macro_inline] def toFamily [FamilyDef Fam a β] (b : β) : Fam a :=
   cast family_key_eq_type.symm b
 
 /-- Cast a datum from its general family to its individual type. -/
-@[macroInline] def ofFamily [FamilyDef Fam a β] (b : Fam a) : β :=
+@[macro_inline] def ofFamily [FamilyDef Fam a β] (b : Fam a) : β :=
   cast family_key_eq_type b
 
 /--
diff --git a/Lake/Util/Opaque.lean b/Lake/Util/Opaque.lean
index a87472dd52..a60486e58f 100644
--- a/Lake/Util/Opaque.lean
+++ b/Lake/Util/Opaque.lean
@@ -38,11 +38,11 @@ macro (name := hydrateOpaqueType)
   `(
   namespace $oty
   unsafe def $unsafeMk : $ty $args* → $oty $args* := unsafeCast
-  @[implementedBy $unsafeMk] opaque $mk : $ty $args* → $oty $args*
+  @[implemented_by $unsafeMk] opaque $mk : $ty $args* → $oty $args*
   instance : Coe ($ty $args*) ($oty $args*) := ⟨$mk⟩
 
   unsafe def $unsafeGet : $oty $args* → $ty $args* := unsafeCast
-  @[implementedBy $unsafeGet] opaque $get $[{$args}]* : $oty $args* → $ty $args*
+  @[implemented_by $unsafeGet] opaque $get $[{$args}]* : $oty $args* → $ty $args*
   instance : Coe ($oty $args*) ($ty $args*) := ⟨$get⟩
 
   instance [Inhabited ($ty $args*)] : Inhabited ($oty $args*) := ⟨$mk default⟩
diff --git a/examples/deps/a/lakefile.lean b/examples/deps/a/lakefile.lean
index ecf4166617..1371c0ce1e 100644
--- a/examples/deps/a/lakefile.lean
+++ b/examples/deps/a/lakefile.lean
@@ -3,4 +3,4 @@ open System Lake DSL
 
 package a
 require root from ".."/"root"
-@[defaultTarget] lean_lib A
+@[default_target] lean_lib A
diff --git a/examples/deps/b/lakefile.lean b/examples/deps/b/lakefile.lean
index 784d438bdf..d975683bf4 100644
--- a/examples/deps/b/lakefile.lean
+++ b/examples/deps/b/lakefile.lean
@@ -3,4 +3,4 @@ open System Lake DSL
 
 package b
 require root from ".."/"root"
-@[defaultTarget] lean_lib B
+@[default_target] lean_lib B
diff --git a/examples/deps/bar/lakefile.lean b/examples/deps/bar/lakefile.lean
index c461c8576a..a180b75b23 100644
--- a/examples/deps/bar/lakefile.lean
+++ b/examples/deps/bar/lakefile.lean
@@ -7,6 +7,6 @@ require foo from ".."/"foo"
 
 lean_lib Bar
 
-@[defaultTarget]
+@[default_target]
 lean_exe bar where
   root := `Main
diff --git a/examples/deps/foo/lakefile.lean b/examples/deps/foo/lakefile.lean
index 9be985aad5..6aad5d9332 100644
--- a/examples/deps/foo/lakefile.lean
+++ b/examples/deps/foo/lakefile.lean
@@ -8,6 +8,6 @@ require b from ".."/"b"
 
 lean_lib Foo
 
-@[defaultTarget]
+@[default_target]
 lean_exe foo where
   root := `Main
diff --git a/examples/deps/root/lakefile.lean b/examples/deps/root/lakefile.lean
index 8b0268df19..198ef3eedc 100644
--- a/examples/deps/root/lakefile.lean
+++ b/examples/deps/root/lakefile.lean
@@ -2,4 +2,4 @@ import Lake
 open Lake DSL
 
 package root
-@[defaultTarget] lean_lib Root
+@[default_target] lean_lib Root
diff --git a/examples/ffi/app/lakefile.lean b/examples/ffi/app/lakefile.lean
index 2f7614f192..7f9f12df52 100644
--- a/examples/ffi/app/lakefile.lean
+++ b/examples/ffi/app/lakefile.lean
@@ -5,7 +5,7 @@ package app
 
 require ffi from ".."/"lib"
 
-@[defaultTarget]
+@[default_target]
 lean_exe app {
   root := `Main
 }
diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean
index 50ceb66259..58870b599b 100644
--- a/examples/ffi/lib/lakefile.lean
+++ b/examples/ffi/lib/lakefile.lean
@@ -8,7 +8,7 @@ package ffi {
 
 lean_lib FFI
 
-@[defaultTarget] lean_exe test {
+@[default_target] lean_exe test {
   root := `Main
 }
 
diff --git a/examples/git/lakefile.lean b/examples/git/lakefile.lean
index a304bc3d2b..30ea391d0f 100644
--- a/examples/git/lakefile.lean
+++ b/examples/git/lakefile.lean
@@ -7,7 +7,7 @@ package git_hello
 require hello from
   git "../.."/"examples"/"hello"
 
-@[defaultTarget]
+@[default_target]
 lean_exe git_hello {
   root := `Main
 }
diff --git a/examples/hello/lakefile.lean b/examples/hello/lakefile.lean
index dbf493210f..6248d47afb 100644
--- a/examples/hello/lakefile.lean
+++ b/examples/hello/lakefile.lean
@@ -5,7 +5,7 @@ package hello
 
 lean_lib Hello
 
-@[defaultTarget]
+@[default_target]
 lean_exe hello {
   root := `Main
 }
diff --git a/examples/precompile/bar/lakefile.lean b/examples/precompile/bar/lakefile.lean
index 91db957c65..be265d5d01 100644
--- a/examples/precompile/bar/lakefile.lean
+++ b/examples/precompile/bar/lakefile.lean
@@ -7,5 +7,5 @@ package bar {
 
 require foo from "../foo"
 
-@[defaultTarget]
+@[default_target]
 lean_lib Bar
diff --git a/examples/precompile/foo/lakefile.lean b/examples/precompile/foo/lakefile.lean
index fff8b18595..66d3529775 100644
--- a/examples/precompile/foo/lakefile.lean
+++ b/examples/precompile/foo/lakefile.lean
@@ -5,5 +5,5 @@ package foo {
   precompileModules := true
 }
 
-@[defaultTarget]
+@[default_target]
 lean_lib foo
diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean
index f09003f58a..701afc3b82 100644
--- a/examples/targets/lakefile.lean
+++ b/examples/targets/lakefile.lean
@@ -5,7 +5,7 @@ package targets {
   srcDir := "src"
 }
 
-@[defaultTarget]
+@[default_target]
 lean_lib foo
 lean_lib bar
 lean_lib baz
@@ -13,10 +13,10 @@ lean_lib baz
 lean_exe a
 lean_exe b
 
-@[defaultTarget]
+@[default_target]
 lean_exe c
 
-@[defaultTarget]
+@[default_target]
 target meow (pkg : Package) : Unit := do
   IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!"
   return .nil
diff --git a/test/102/lakefile.lean b/test/102/lakefile.lean
index 3a2adb36d3..998c16955e 100644
--- a/test/102/lakefile.lean
+++ b/test/102/lakefile.lean
@@ -5,7 +5,7 @@ package tba {
   -- add package configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_lib TBA := {
   name := `TBA
   globs := #[.andSubmodules `TBA]
diff --git a/test/104/test/lakefile.lean b/test/104/test/lakefile.lean
index 41340823c2..e2237a6d49 100644
--- a/test/104/test/lakefile.lean
+++ b/test/104/test/lakefile.lean
@@ -11,7 +11,7 @@ def url : String :=
 
 require hello from git url / "examples" / "hello"
 
-@[defaultTarget]
+@[default_target]
 lean_exe test {
   root := `Main
 }
diff --git a/test/50/foo/lakefile.lean b/test/50/foo/lakefile.lean
index 9138379695..c0e7b9f426 100644
--- a/test/50/foo/lakefile.lean
+++ b/test/50/foo/lakefile.lean
@@ -5,5 +5,5 @@ package foo where
   moreLeanArgs := get_config? leanArgs |>.getD "" |>.splitOn " " |>.toArray
   moreLeancArgs := get_config? leancArgs |>.getD "" |>.splitOn " " |>.toArray
 
-@[defaultTarget]
+@[default_target]
 lean_exe foo
diff --git a/test/75/foo/lakefile.lean b/test/75/foo/lakefile.lean
index 08f86f0fb3..bc5ee700db 100644
--- a/test/75/foo/lakefile.lean
+++ b/test/75/foo/lakefile.lean
@@ -9,7 +9,7 @@ lean_lib Foo {
   -- add library configuration options here
 }
 
-@[defaultTarget]
+@[default_target]
 lean_exe foo {
   root := `Main
 }