diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 61942d1d15..85b1155979 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -5,39 +5,39 @@ Authors: Leonardo de Moura
 -/
 import Lean.Util.FoldConsts
 import Lean.Elab.Command
-
+new_frontend
 namespace Lean
 namespace Elab
 namespace Command
 
 private def throwUnknownId (id : Name) : CommandElabM Unit :=
-throwError ("unknown identifier '" ++ toString id ++ "'")
+throwError! "unknown identifier '{id}'"
 
 private def lparamsToMessageData (lparams : List Name) : MessageData :=
 match lparams with
 | []    => ""
-| u::us =>
-  let m : MessageData := ".{" ++ u;
-  let m := us.foldl (fun (s : MessageData) u => s ++ ", " ++ u) m;
-  m ++ "}"
+| u::us => do
+  let m : MessageData := ".{" ++ u
+  for u in us do
+    m := m ++ ", " ++ u
+  return m ++ "}"
 
 private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := do
-let m : MessageData := if isUnsafe then "unsafe " else "";
-env ← getEnv;
-let m := if isProtected env id then m ++ "protected " else m;
+let m : MessageData := if isUnsafe then "unsafe " else ""
+let m := if isProtected (← getEnv) id then m ++ "protected " else m
 let (m, id) := match privateToUserName? id : _ → MessageData × Name with
   | some id => (m ++ "private ", id)
-  | none    => (m, id);
-let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type;
+  | none    => (m, id)
+let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
 pure m
 
 private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
-m ← mkHeader kind id lparams type isUnsafe;
-let m := m ++ " :=" ++ Format.line ++ value;
+let m ← mkHeader kind id lparams type isUnsafe
+let m := m ++ " :=" ++ Format.line ++ value
 logInfo m
 
 private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
-m ← mkHeader kind id lparams type isUnsafe;
+let m ← mkHeader kind id lparams type isUnsafe
 logInfo m
 
 private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
@@ -45,19 +45,15 @@ printAxiomLike "Quotient primitive" id lparams type
 
 private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
-env ← getEnv;
-m ← mkHeader "inductive" id lparams type isUnsafe;
-let m := m ++ Format.line ++ "constructors:";
-m ← ctors.foldlM
-  (fun (m : MessageData) ctor => do
-    cinfo ← getConstInfo ctor;
-    pure $ m ++ Format.line ++ ctor ++ " : " ++ cinfo.type)
-  m;
+let m ← mkHeader "inductive" id lparams type isUnsafe
+let m := m ++ Format.line ++ "constructors:"
+for ctor in ctors do
+  let cinfo ← getConstInfo ctor
+  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
 logInfo m
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
-env ← getEnv;
-match env.find? id with
+match (← getEnv).find? id with
 | ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
 | ConstantInfo.defnInfo  { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
 | ConstantInfo.thmInfo  { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
@@ -70,14 +66,14 @@ match env.find? id with
 | none => throwUnknownId id
 
 private def printId (id : Name) : CommandElabM Unit := do
-cs ← resolveGlobalConst id;
+let cs ← resolveGlobalConst id
 cs.forM printIdCore
 
 @[builtinCommandElab «print»] def elabPrint : CommandElab :=
 fun stx =>
-  let numArgs := stx.getNumArgs;
+  let numArgs := stx.getNumArgs
   if numArgs == 2 then
-    let arg := stx.getArg 1;
+    let arg := stx.getArg 1
     if arg.isIdent then
       printId arg.getId
     else match arg.isStrLit? with
@@ -89,18 +85,18 @@ fun stx =>
 namespace CollectAxioms
 
 structure State :=
-(visited : NameSet := {})
+(visited : NameSet    := {})
 (axioms  : Array Name := #[])
 
 abbrev M := ReaderT Environment $ StateM State
 
 partial def collect : Name → M Unit
 | c => do
-  let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect;
-  s ← get;
-  unless (s.visited.contains c) do
-    modify fun s => { s with visited := s.visited.insert c };
-    env ← read;
+  let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
+  let s ← get
+  unless s.visited.contains c do
+    modify fun s => { s with visited := s.visited.insert c }
+    let env ← read
     match env.find? c with
     | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push c }
     | some (ConstantInfo.defnInfo v)   => collectExpr v.type *> collectExpr v.value
@@ -115,19 +111,17 @@ partial def collect : Name → M Unit
 end CollectAxioms
 
 private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
-env ← getEnv;
-let (_, s) := ((CollectAxioms.collect constName).run env).run {};
+let env ← getEnv
+let (_, s) := ((CollectAxioms.collect constName).run env).run {}
 if s.axioms.isEmpty then
-  logInfo ("'" ++ constName ++ "' does not depend on any axioms")
+  logInfo msg!"'{constName}' does not depend on any axioms"
 else
-  logInfo ("'" ++ constName ++ "' depends on axioms: " ++ toString s.axioms.toList)
+  logInfo msg!"'{constName}' depends on axioms: {s.axioms.toList}"
 
 @[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab :=
 fun stx => do
-  let id := (stx.getArg 2).getId;
-  cs ← resolveGlobalConst id;
+  let id := (stx.getArg 2).getId
+  let cs ← resolveGlobalConst id
   cs.forM printAxiomsOf
 
-end Command
-end Elab
-end Lean
+end Lean.Elab.Command
diff --git a/src/Lean/Elab/StrategyAttrs.lean b/src/Lean/Elab/StrategyAttrs.lean
index 40c590a603..9dd037d870 100644
--- a/src/Lean/Elab/StrategyAttrs.lean
+++ b/src/Lean/Elab/StrategyAttrs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Attributes
+new_frontend
 
 namespace Lean
 /-
@@ -17,14 +18,11 @@ inductive ElaboratorStrategy
 instance ElaboratorStrategy.inhabited : Inhabited ElaboratorStrategy :=
 ⟨ElaboratorStrategy.withExpectedType⟩
 
-def mkElaboratorStrategyAttrs : IO (EnumAttributes ElaboratorStrategy) :=
-registerEnumAttributes `elaboratorStrategy
-  [(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
-   (`elabSimple, "instructs elaborator that the arguments of the function application (f ...) should be elaborated from left to right, and without propagating information from the expected type to its arguments", ElaboratorStrategy.simple),
-   (`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
-
-@[init mkElaboratorStrategyAttrs]
-constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := arbitrary _
+initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
+  registerEnumAttributes `elaboratorStrategy
+    [(`elabWithExpectedType, "instructs elaborator that the arguments of the function application (f ...) should be elaborated using information about the expected type", ElaboratorStrategy.withExpectedType),
+     (`elabSimple, "instructs elaborator that the arguments of the function application (f ...) should be elaborated from left to right, and without propagating information from the expected type to its arguments", ElaboratorStrategy.simple),
+     (`elabAsEliminator, "instructs elaborator that the arguments of the function application (f ...) should be elaborated as f were an eliminator", ElaboratorStrategy.asEliminator)]
 
 @[export lean_get_elaborator_strategy]
 def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index e62d96e866..b16b1436c8 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -7,6 +7,7 @@ import Lean.Util.Trace
 import Lean.Parser.Extension
 import Lean.KeyedDeclsAttribute
 import Lean.Elab.Exception
+new_frontend
 
 namespace Lean
 
@@ -16,12 +17,13 @@ match stx.unsetTrailing.reprint with -- TODO use syntax pretty printer
 | none     => format stx
 
 def MacroScopesView.format (view : MacroScopesView) (mainModule : Name) : Format :=
-format $
-  if view.scopes.isEmpty then view.name
+fmt $
+  if view.scopes.isEmpty then
+    view.name
   else if view.mainModule == mainModule then
-   view.scopes.foldl mkNameNum (view.name ++ view.imported)
+    view.scopes.foldl mkNameNum (view.name ++ view.imported)
   else
-   view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
+    view.scopes.foldl mkNameNum (view.name ++ view.imported ++ view.mainModule)
 
 namespace Elab
 
@@ -35,51 +37,49 @@ def getBetterRef (ref : Syntax) (macroStack : MacroStack) : Syntax :=
 match ref.getPos with
 | some _ => ref
 | none   =>
-  match macroStack.find? $ fun (elem : MacroStackElem) => elem.before.getPos != none with
+  match macroStack.find? (·.before.getPos != none) with
   | some elem => elem.before
   | none      => ref
 
 def ppMacroStackDefault := false
-@[init] def ppMacroStackOption : IO Unit :=
-registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
 def getMacroStackOption (o : Options) : Bool:= o.get `pp.macroStack ppMacroStackDefault
 def setMacroStackOption (o : Options) (flag : Bool) : Options := o.setBool `pp.macroStack flag
+initialize
+  registerOption `pp.macroStack { defValue := ppMacroStackDefault, group := "pp", descr := "dispaly macro expansion stack" }
 
 def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroStack : MacroStack) : m MessageData := do
-options ← getOptions;
-if !getMacroStackOption options then pure msgData else
+if !getMacroStackOption (← getOptions) then pure msgData else
 match macroStack with
 | []             => pure msgData
 | stack@(top::_) =>
-  let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ top.after);
+  let msgData := msgData ++ Format.line ++ "with resulting expansion" ++ MessageData.nest 2 (Format.line ++ top.after)
   pure $ stack.foldl
     (fun (msgData : MessageData) (elem : MacroStackElem) =>
       msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ elem.before))
     msgData
 
 def checkSyntaxNodeKind (k : Name) : AttrM Name := do
-env ← getEnv;
-if Parser.isValidSyntaxNodeKind env k then pure k
+if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k
 else throwError "failed"
 
 namespace OldFrontend -- TODO: delete
 
 private def checkSyntaxNodeKindAtNamespacesAux (k : Name) : List Name → AttrM Name
 | []    => throwError "failed"
-| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux ns
+| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k ns
 
 def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
-env ← getEnv;
+let env ← getEnv
 checkSyntaxNodeKindAtNamespacesAux k (Lean.TODELETE.getNamespaces env)
 
 end OldFrontend
 
 def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name
-| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux p
+| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k p
 | _ => throwError "failed"
 
 def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
-ctx ← read;
+let ctx ← read
 checkSyntaxNodeKindAtNamespacesAux k ctx.currNamespace
 
 def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (arg : Syntax) : AttrM SyntaxNodeKind :=
@@ -93,8 +93,8 @@ match attrParamSyntaxToIdentifier arg with
   <|>
   checkSyntaxNodeKind (defaultParserNamespace ++ k)
   <|>
-  throwError ("invalid syntax node kind '" ++ toString k ++ "'")
-| none   => throwError ("syntax node kind is missing")
+  throwError! "invalid syntax node kind '{k}'"
+| none   => throwError "syntax node kind is missing"
 
 private unsafe def evalSyntaxConstantUnsafe (env : Environment) (constName : Name) : ExceptT String Id Syntax :=
 env.evalConstCheck Syntax `Lean.Syntax constName
@@ -107,31 +107,34 @@ private constant evalConstant (γ : Type) (env : Environment) (typeName : Name)
 unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String)
     : IO (KeyedDeclsAttribute γ) :=
 KeyedDeclsAttribute.init {
-  builtinName := attrBuiltinName,
-  name := attrName,
-  descr := kind ++ " elaborator",
+  builtinName   := attrBuiltinName,
+  name          := attrName,
+  descr         := kind ++ " elaborator",
   valueTypeName := typeName,
-  evalKey := fun _ arg => syntaxNodeKindOfAttrParam parserNamespace arg,
+  evalKey       := fun _ arg => syntaxNodeKindOfAttrParam parserNamespace arg,
 } attrDeclName
 
-unsafe def mkMacroAttribute : IO (KeyedDeclsAttribute Macro) :=
+unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
 mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro"
-@[init mkMacroAttribute] constant macroAttribute : KeyedDeclsAttribute Macro := arbitrary _
+
+@[implementedBy mkMacroAttributeUnsafe]
+constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro) := arbitrary _
+
+initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
 
 private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
 | []    => throw Macro.Exception.unsupportedSyntax
-| m::ms =>
+| m::ms => do
+  try
+    m stx
   catch
-    (m stx)
-    (fun ex =>
-      match ex with
-      | Macro.Exception.unsupportedSyntax => expandMacroFns ms
-      | ex                                => throw ex)
+    | Macro.Exception.unsupportedSyntax => expandMacroFns stx ms
+    | ex                                => throw ex
 
 def getMacros (env : Environment) : Macro :=
 fun stx =>
-  let k := stx.getKind;
-  let table := (macroAttribute.ext.getState env).table;
+  let k := stx.getKind
+  let table := (macroAttribute.ext.getState env).table
   match table.find? k with
   | some macroFns => expandMacroFns stx macroFns
   | none          => throw Macro.Exception.unsupportedSyntax
@@ -147,32 +150,31 @@ instance monadMacroAdapterTrans (m n) [MonadMacroAdapter m] [MonadLift m n] : Mo
   setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _) }
 
 private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syntax) := do
+try
+  let newStx ← getMacros env stx
+  pure (some newStx)
 catch
-  (do newStx ← getMacros env stx; pure (some newStx))
-  (fun ex => match ex with
-    | Macro.Exception.unsupportedSyntax => pure none
-    | _                                 => throw ex)
+  | Macro.Exception.unsupportedSyntax => pure none
+  | ex                                => throw ex
 
 @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
     [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : MacroM α) : m α := do
-scp  ← MonadMacroAdapter.getCurrMacroScope;
-env  ← getEnv;
-next ← MonadMacroAdapter.getNextMacroScope;
-currRecDepth ← MonadRecDepth.getRecDepth;
-maxRecDepth ← MonadRecDepth.getMaxRecDepth;
-match x { macroEnv := Macro.mkMacroEnv (expandMacro? env),
-          currMacroScope := scp, mainModule := env.mainModule, currRecDepth := currRecDepth, maxRecDepth := maxRecDepth } next with
+let env  ← getEnv
+match x { macroEnv       := Macro.mkMacroEnv (expandMacro? env),
+          currMacroScope := ← MonadMacroAdapter.getCurrMacroScope,
+          mainModule     := env.mainModule,
+          currRecDepth   := ← MonadRecDepth.getRecDepth,
+          maxRecDepth    := ← MonadRecDepth.getMaxRecDepth } (← MonadMacroAdapter.getNextMacroScope) with
 | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
 | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg
-| EStateM.Result.ok a nextMacroScope                       => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
+| EStateM.Result.ok a nextMacroScope                       => MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
 
 @[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
     [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
 liftMacroM (x stx)
 
-@[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Elab;
-registerTraceClass `Elab.step
+initialize
+  registerTraceClass `Elab
+  registerTraceClass `Elab.step
 
-end Elab
-end Lean
+end Lean.Elab