Access Tactic State

Stream: general

[Mohammed Eyad Kurd-Misto]

Is there any way to retrieve the tactic state during some point in a proof? I.E. as a string or some kind of object that would include the goals of the current tactic state.

[Jason Rute]

Do you just want to trace it? If so, just do trace_state.

[Jason Rute]

If you want a string or list of goals, there are a few approaches.

[Jason Rute]

Assuming you are familiar with "monadology":

meta def get_state_string : tactic string :=
do
  state <- tactic.read,
  fmt <- tactic.pp state,
  return (to_string fmt)

meta def trace_state_string : tactic unit :=
do
  state_string <- get_state_string,
  tactic.trace state_string

example (n : nat) : n = n := begin
induction n,
-- built in trace state
trace_state,
-- our reimplementation
trace_state_string,
-- rest of proof
simp,
simp
end

[Jason Rute]

More advanced things you can do are:

• get strings for individual goals or hypotheses
• get strings for the types of the hypotheses in the local context
• change how the pretty printer prints goals

These all get a little trickier.

[Kyle Miller]

@Mohammed Eyad Kurd-Misto Are you looking for tactic#extract_goal?

[Jason Rute]

@Kyle Miller I'm curious. How robust is extract_goal? I once tried to recreate something like that, but I found it often didn't round trip very well. It was easy to create an example string which couldn't be entered into Lean. (Of course, maybe my goals at the time were too ambitious. It probably works well for a lot of use cases.)

[Scott Morrison]

I think it has exactly the same set of problems as round-tripping pp does.

[Scott Morrison]

In particular, I've not heard of any problems to do with setting up the arguments.

[Mohammed Eyad Kurd-Misto]

@Kyle Miller That looks perfect, thank you!

[Mohammed Eyad Kurd-Misto]

@Jason Rute extract_goal looks like it might do what I need but if not this seems helpful, thank you!