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

fix: Elab.postpone trace message

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-18 11:52:47 -07:00
parent 40ed0de071
commit 285658cead
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/SyntheticMVars.lean
View file

@ -135,7 +135,8 @@ modify fun s => { s with syntheticMVars := [] }
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do
trace[Elab.postpone]! "resuming ?{mvarDecl.mvarId}"
-- We use `traceM` because we want to make sure the metavar local context is used to trace the message
traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext msg!"resuming {mkMVar mvarDecl.mvarId}")
let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
pure !succeeded