perf: make trace[...] ... notation lazy

src/Lean/Elab/Command.lean

@@ -215,9 +215,7 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : Std.Persisten
   let tree := InfoTree.context {
     env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
   } tree
-  if checkTraceOption (← getOptions) `Elab.info then
-    let fmt ← tree.format
-    trace[Elab.info] fmt
+  trace[Elab.info] ← tree.format
   return tree
 
 private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit

src/Lean/Meta/Match/Match.lean

@@ -542,7 +542,7 @@ private def expandNatValuePattern (p : Problem) : Problem := do
     | _                                                     => alt
   { p with alts := alts }
 
-private def traceStep (msg : String) : StateRefT State MetaM Unit :=
+private def traceStep (msg : String) : StateRefT State MetaM Unit := do
   trace[Meta.Match.match] "{msg} step"
 
 private def traceState (p : Problem) : MetaM Unit :=

src/Lean/Util/Trace.lean

@@ -135,15 +135,12 @@ end
 def registerTraceClass (traceClassName : Name) : IO Unit :=
   registerOption (`trace ++ traceClassName) { group := "trace", defValue := false, descr := "enable/disable tracing for the given module and submodules" }
 
-syntax "trace[" ident "]" (interpolatedStr(term) <|> term) : term
-
-macro_rules
-  | `(trace[$id] $s) =>
-    if s.getKind == interpolatedStrKind then
-      `(Lean.trace $(quote id.getId) fun _ => m! $s)
-    else
-      `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
-
+macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $s) else `(($s : MessageData))
+  `(doElem| do
+    let cls := $(quote id.getId)
+    if (← Lean.isTracingEnabledFor cls) then
+      Lean.addTrace cls $msg)
 
 private def withNestedTracesFinalizer [Monad m] [MonadTrace m] (ref : Syntax) (currTraces : PersistentArray TraceElem) : m Unit := do
   modifyTraces fun traces =>

tests/lean/run/meta2.lean

@@ -7,7 +7,7 @@ open Lean.Meta
 -- set_option trace.Meta.isDefEq.delta false
 set_option trace.Meta.debug true
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=

tests/lean/run/meta3.lean

@@ -9,7 +9,7 @@ let opt := opt.setBool `trace.Meta true;
 -- let opt := opt.setBool `trace.Meta.check false;
 opt
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def check (x : MetaM Bool) : MetaM Unit :=

tests/lean/run/meta4.lean

@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=

tests/lean/run/meta6.lean

@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=

tests/lean/run/meta7.lean

@@ -10,7 +10,7 @@ partial def fact : Nat → Nat
 set_option trace.Meta.debug true
 set_option trace.Meta.check false
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def checkM (x : MetaM Bool) : MetaM Unit :=

tests/lean/run/recInfo1.lean

@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.debug] msg
 
 def showRecInfo (declName : Name) (majorPos? : Option Nat := none) : MetaM Unit := do

tests/lean/run/synth1.lean

@@ -24,7 +24,7 @@ instance coerceNatToBool : HasCoerce Nat Bool :=
 instance coerceNatToInt : HasCoerce Nat Int :=
 ⟨fun x => Int.ofNat x⟩
 
-def print {α} [ToString α] (a : α) : MetaM Unit :=
+def print {α} [ToString α] (a : α) : MetaM Unit := do
 trace[Meta.synthInstance] (toString a)
 
 

tests/lean/run/tactic.lean

@@ -6,7 +6,7 @@ open Lean.Meta
 
 axiom simple : forall {p q : Prop}, p → q → p
 
-def print (msg : MessageData) : MetaM Unit :=
+def print (msg : MessageData) : MetaM Unit := do
 trace[Meta.Tactic] msg
 
 def tst1 : MetaM Unit := do

tests/lean/run/trace.lean

@@ -38,6 +38,8 @@ do traceCtx `module $ do {
    -- Messages are computed lazily. The following message will only be computed
    -- if `trace.slow is active.
    trace[slow] (m!"slow message: " ++ toString (slow b))
+   -- This is true even if it is a monad computation:
+   trace[slow] (m!"slow message: " ++ (← toString (slow b)))
 
 def run (x : M Unit) : M Unit :=
 withReader