analogue of `trace_state`

Stream: lean4

[Scott Morrison]

Is there a Lean4 analogue of trace_state, which just prints the current goal state? (In TacticM.)

[Mario Carneiro]

trace_state is a lean 4 tactic, so the DIY answer is to find out what it does

[Mario Carneiro]

you find the following:

@[builtinTactic traceState] def evalTraceState : Tactic := fun _ => do
  let gs ← getUnsolvedGoals
  withPPForTacticGoal <| addRawTrace (goalsToMessageData gs)

but the most important part is that you use goalsToMessageData and then print it. I would just do logInfo (goalsToMessageData (<- getGoals))

[Mario Carneiro]

if you just pass an MVarId to throwError or logInfo m!"..." the results are surprisingly readable