approach 1 *seems* to work

Author: datokrat

src/Lean/Elab/SyntheticMVars.lean

@@ -37,16 +37,14 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
         let mvarDecl     ← getMVarDecl mvarId
         let expectedType ← instantiateMVars mvarDecl.type
         let ret ← withInfoHole mvarId do
-          logInfo m!"resumeElabTerm..."
           let result ← resumeElabTerm stx expectedType (!postponeOnError)
           /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
             That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
-          logInfo m!"ensureHasType..."
           let result ← do
             if (← getInfoState).enabled then
               let savedInfoTrees ← getResetInfoTrees
               -- withRef stx <| ensureHasType expectedType result
-              Prod.fst <$> MonadFinally.tryFinally' (withRef stx <| ensureHasType expectedType result) fun a? => do
+              Prod.fst <$> MonadFinally.tryFinally' (withRef stx <| ensureHasType expectedType result) fun _ => do
                 modifyInfoState fun state =>
                   if savedInfoTrees.size > 0 then
                     let mod (t : InfoTree) : InfoTree :=
@@ -58,9 +56,6 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
                     { state with trees := savedInfoTrees }
             else
               withRef stx <| ensureHasType expectedType result
-          let trees ← getInfoTrees
-          let strs ← trees.toArray.mapM (·.format')
-          logInfo m!"withInfoHole inner {strs}"
           /- We must perform `occursCheck` here since `result` may contain `mvarId` when it has synthetic `sorry`s. -/
           if (← occursCheck mvarId result) then
             mvarId.assign result

src/Lean/Elab/Term/TermElabM.lean

@@ -1208,17 +1208,10 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
     withoutMacroStackAtErr do
       match ← coerce? e expectedType with
       | .some eNew =>
-        let trees ← getInfoTrees
-        let strs ← trees.toArray.mapM (fun t => do return (← t.format'))
-        logInfo m!"{strs}"
         pushInfoLeaf (.ofCustomInfo {
           stx := ← getRef
           value := Dynamic.mk <| CoeExpansionTrace.mk []
         })
-        logInfo m!"pushed info leaf"
-        let trees ← getInfoTrees
-        let strs ← trees.toArray.mapM (fun t => do return (← t.format'))
-        logInfo m!"{strs}"
         return eNew
       | .none => failure
       | .undef =>
@@ -1529,7 +1522,6 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
   | (elabFn::elabFns) =>
     try
       -- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
-      logInfo m!"enter term info context for {stx}"
       let ret ← withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
         (try
           elabFn.value stx expectedType?
@@ -1563,7 +1555,6 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
               postponeElabTermCore stx expectedType?
             else
               throw ex)
-      logInfo m!"leave term info context for {stx}"
       pure ret
     catch ex => match ex with
       | .internal id _ =>

tests/lean/run/test.lean

@@ -1,6 +1,5 @@
 structure X
 def X.x (_ : X) : BaseIO Bool := sorry
 
-set_option trace.Elab.info true
 def f : IO Unit := do
   let _ ← ([] : List X).findM? fun p => p.x