fix: trace_state messages should not be lost during backtracking

src/Lean/Elab/Tactic/Basic.lean

@@ -175,7 +175,7 @@ mutual
     expandTacticMacroFns stx (macroAttribute.getEntries (← getEnv) stx.getKind)
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
-    withRef stx <| withIncRecDepth <| withFreshMacroScope $ match stx with
+    withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
       | Syntax.node _ k args =>
         if k == nullKind then
           -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -129,7 +129,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do
   let gs ← getUnsolvedGoals
-  logInfo (goalsToMessageData gs)
+  addRawTrace (goalsToMessageData gs)
 
 @[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx =>
   liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure []

src/Lean/Util/Trace.lean

@@ -101,15 +101,22 @@ private def getResetTraces : m (PersistentArray TraceElem) := do
 section
 variable [MonadRef m] [AddMessageContext m] [MonadOptions m]
 
+private def addTraceOptions (msg : MessageData) : MessageData :=
+  match msg with
+  | MessageData.withContext ctx msg => MessageData.withContext { ctx with opts := ctx.opts.setBool `pp.analyze false } msg
+  | msg => msg
+
+def addRawTrace (msg : MessageData) : m Unit := do
+  let ref ← getRef
+  let msg ← addMessageContext msg
+  let msg := addTraceOptions msg
+  modifyTraces fun traces => traces.push { ref, msg }
+
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
   let ref ← getRef
   let msg ← addMessageContext msg
   let msg := addTraceOptions msg
   modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged (cls ++ `_traceMsg) m!"[{cls}] {msg}" }
-where
-  addTraceOptions : MessageData → MessageData
-    | MessageData.withContext ctx msg => MessageData.withContext { ctx with opts := ctx.opts.setBool `pp.analyze false } msg
-    | msg => msg
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if (← isTracingEnabledFor cls) then

tests/lean/1027.lean.expected.out

@@ -1,4 +1,4 @@
+1027.lean:4:2-4:7: warning: declaration uses 'sorry'
 x : Nat
 h : ¬x = 0
 ⊢ Unit
-1027.lean:4:2-4:7: warning: declaration uses 'sorry'

tests/lean/690.lean.expected.out

@@ -2,16 +2,16 @@
 690.lean:3:2-3:29: error: too many variable names provided at alternative 'step', #3 provided, but #2 expected
 690.lean:3:24-3:29: warning: declaration uses 'sorry'
 690.lean:9:12-9:17: warning: declaration uses 'sorry'
+690.lean:8:34-8:39: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
 hStep : Nat.le a m✝
 ih : Nat.le a (m✝ + 1)
 ⊢ Nat.le a (Nat.succ m✝ + 1)
-690.lean:8:34-8:39: warning: declaration uses 'sorry'
 690.lean:14:12-14:17: warning: declaration uses 'sorry'
+690.lean:13:37-13:42: warning: declaration uses 'sorry'
 case step
 a b x : Nat
 hStep : Nat.le a x
 ih : Nat.le a (x + 1)
 ⊢ Nat.le a (Nat.succ x + 1)
-690.lean:13:37-13:42: warning: declaration uses 'sorry'

tests/lean/consumePPHint.lean.expected.out

@@ -1,6 +1,6 @@
 consumePPHint.lean:4:30-4:35: warning: declaration uses 'sorry'
+consumePPHint.lean:10:2-10:7: warning: declaration uses 'sorry'
 case a
 ⊢ q
     (let_fun x := 0;
     x + 1)
-consumePPHint.lean:10:2-10:7: warning: declaration uses 'sorry'

tests/lean/convInConv.lean.expected.out

@@ -6,6 +6,7 @@ x : Nat
 ⊢ x
 x : Nat
 ⊢ id (twice x)
+convInConv.lean:25:2-25:7: warning: declaration uses 'sorry'
 y : Nat
 ⊢ (fun x => x + y = 0) = fun x => False
 y : Nat
@@ -16,4 +17,3 @@ y : Nat
 ⊢ (fun x => y + x = 0) = fun x => False
 y : Nat
 ⊢ (fun x => y + x = 0) = fun x => False
-convInConv.lean:25:2-25:7: warning: declaration uses 'sorry'

tests/lean/inductionGen.lean.expected.out

@@ -1,5 +1,6 @@
 inductionGen.lean:23:2-23:14: error: index in target's type is not a variable (consider using the `cases` tactic instead)
   n + 1
+inductionGen.lean:29:11-29:16: warning: declaration uses 'sorry'
 case cons
 α : Type u_1
 n : Nat
@@ -8,7 +9,10 @@ x : α
 xs : Vec α n
 h : Vec.cons x xs = ys
 ⊢ Vec.head (Vec.cons x xs) = Vec.head ys
-inductionGen.lean:29:11-29:16: warning: declaration uses 'sorry'
+inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
+inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
+inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
+inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
 case natVal
 α : ExprType
 a✝ : Nat
@@ -40,7 +44,3 @@ a✝¹ a✝ : Expr ExprType.nat
 b : Expr ExprType.nat
 h : Expr.add a✝¹ a✝ = b
 ⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b
-inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
-inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
-inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'
-inductionGen.lean:68:9-68:14: warning: declaration uses 'sorry'

tests/lean/renameI.lean.expected.out

@@ -1,9 +1,9 @@
+renameI.lean:5:2-5:7: warning: declaration uses 'sorry'
 x y : Nat
 ⊢ x = y
-renameI.lean:5:2-5:7: warning: declaration uses 'sorry'
+renameI.lean:11:2-11:7: warning: declaration uses 'sorry'
 x a.b : Nat
 ⊢ x = a.b
-renameI.lean:11:2-11:7: warning: declaration uses 'sorry'
+renameI.lean:17:2-17:7: warning: declaration uses 'sorry'
 x o✝ y a.b : Nat
 ⊢ x + y = a.b + o✝
-renameI.lean:17:2-17:7: warning: declaration uses 'sorry'

tests/lean/rwWithoutOffsetCnstrs.lean.expected.out

@@ -1,3 +1,3 @@
+rwWithoutOffsetCnstrs.lean:8:2-8:7: warning: declaration uses 'sorry'
 m n : Nat
 ⊢ Nat.ble (n + 1) n = false
-rwWithoutOffsetCnstrs.lean:8:2-8:7: warning: declaration uses 'sorry'

tests/lean/traceStateBactracking.lean

@@ -0,0 +1,2 @@
+example (h : 0 = 1) : False := by
+  first | trace_state; fail | contradiction

tests/lean/traceStateBactracking.lean.expected.out

@@ -0,0 +1,2 @@
+h : 0 = 1
+⊢ False