dbg_trace flickering

Stream: lean4

[Damiano Testa]

I have always observed that dbg_trace is a little unstable. As it is a debugging tool, maybe this is not especially important.

Below is a reproducible example of a "flickering" behaviour, in case anyone is interested in this.

File edits affect whether or not dbg_trace shows its message on example.

import Lean.Elab.Command

-- If there is no `dbg_trace` message, add a line break here or a space
-- in most places before `rfl`
example : 0 = 0 := by
  run_tac
    dbg_trace "Hello"
  rfl -- add a space after `rfl` and the `dbg_trace` message disappears