From 63a5cd5056d140637add3379b0cf2e1847dd24be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Feb 2022 11:07:41 -0800 Subject: [PATCH] fix: `trace_state` messages should not be lost during backtracking --- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 2 +- src/Lean/Util/Trace.lean | 15 +++++++++++---- tests/lean/1027.lean.expected.out | 2 +- tests/lean/690.lean.expected.out | 4 ++-- tests/lean/consumePPHint.lean.expected.out | 2 +- tests/lean/convInConv.lean.expected.out | 2 +- tests/lean/inductionGen.lean.expected.out | 10 +++++----- tests/lean/renameI.lean.expected.out | 6 +++--- .../lean/rwWithoutOffsetCnstrs.lean.expected.out | 2 +- tests/lean/traceStateBactracking.lean | 2 ++ .../lean/traceStateBactracking.lean.expected.out | 2 ++ 12 files changed, 31 insertions(+), 20 deletions(-) create mode 100644 tests/lean/traceStateBactracking.lean create mode 100644 tests/lean/traceStateBactracking.lean.expected.out diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index f9377f3a01..663567bde8 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/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ₙ]` diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 2b8a595d25..21d54e8182 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/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 [] diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 24a53719cd..15ede7a70f 100644 --- a/src/Lean/Util/Trace.lean +++ b/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 diff --git a/tests/lean/1027.lean.expected.out b/tests/lean/1027.lean.expected.out index d9591e0818..c45e77c1bc 100644 --- a/tests/lean/1027.lean.expected.out +++ b/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' diff --git a/tests/lean/690.lean.expected.out b/tests/lean/690.lean.expected.out index 44bf004199..cb770487bf 100644 --- a/tests/lean/690.lean.expected.out +++ b/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' diff --git a/tests/lean/consumePPHint.lean.expected.out b/tests/lean/consumePPHint.lean.expected.out index f793a997c5..8d36cadca0 100644 --- a/tests/lean/consumePPHint.lean.expected.out +++ b/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' diff --git a/tests/lean/convInConv.lean.expected.out b/tests/lean/convInConv.lean.expected.out index 713c2cb60b..6599b6adc0 100644 --- a/tests/lean/convInConv.lean.expected.out +++ b/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' diff --git a/tests/lean/inductionGen.lean.expected.out b/tests/lean/inductionGen.lean.expected.out index 463d766809..8a48f4d290 100644 --- a/tests/lean/inductionGen.lean.expected.out +++ b/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' diff --git a/tests/lean/renameI.lean.expected.out b/tests/lean/renameI.lean.expected.out index 74e56d56d3..420ae5eed6 100644 --- a/tests/lean/renameI.lean.expected.out +++ b/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' diff --git a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out b/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out index e4435b8217..949c826b82 100644 --- a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out +++ b/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' diff --git a/tests/lean/traceStateBactracking.lean b/tests/lean/traceStateBactracking.lean new file mode 100644 index 0000000000..ec5a4ba9f0 --- /dev/null +++ b/tests/lean/traceStateBactracking.lean @@ -0,0 +1,2 @@ +example (h : 0 = 1) : False := by + first | trace_state; fail | contradiction diff --git a/tests/lean/traceStateBactracking.lean.expected.out b/tests/lean/traceStateBactracking.lean.expected.out new file mode 100644 index 0000000000..0b6f1f21b1 --- /dev/null +++ b/tests/lean/traceStateBactracking.lean.expected.out @@ -0,0 +1,2 @@ +h : 0 = 1 +⊢ False