max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: trace for backtracked tactic exceptions

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-22 18:25:13 +02:00 • committed by Leonardo de Moura
parent 5e9ca825d1
commit 40c1bde7f1
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/Basic.lean
View file

@ -172,6 +172,7 @@ where
@[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → TacticM Unit) := do
match ex with
| .error .. =>
trace[Elab.tactic.backtrack] ex.toMessageData
let failures := failures.push ⟨ex, ← Tactic.saveState⟩
s.restore (restoreInfo := true); k failures
| .internal id _ =>
@ -179,6 +180,8 @@ where
-- We do not store `unsupportedSyntaxExceptionId`, see throwExs
s.restore (restoreInfo := true); k failures
else if id == abortTacticExceptionId then
for msg in (← Core.getMessageLog).toList do
trace[Elab.tactic.backtrack] msg.data
let failures := failures.push ⟨ex, ← Tactic.saveState⟩
s.restore (restoreInfo := true); k failures
else
@ -417,5 +420,6 @@ def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :
withRef (mkNullNode #[arrow, body]) x
builtin_initialize registerTraceClass `Elab.tactic
builtin_initialize registerTraceClass `Elab.tactic.backtrack
end Lean.Elab.Tactic