Zulip Chat Archive

Stream: general

Topic: Access Tactic State

Mohammed Eyad Kurd-Misto (Jul 10 2020 at 03:10):

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 (Jul 10 2020 at 03:27):

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

Jason Rute (Jul 10 2020 at 03:29):

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

Jason Rute (Jul 10 2020 at 03:44):

Assuming you are familiar with "monadology":

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

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

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

Jason Rute (Jul 10 2020 at 03:47):

More advanced things you can do are:

These all get a little trickier.

Kyle Miller (Jul 10 2020 at 03:54):

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

Jason Rute (Jul 10 2020 at 03:59):

@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 (Jul 10 2020 at 04:09):

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

Scott Morrison (Jul 10 2020 at 04:10):

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

Mohammed Eyad Kurd-Misto (Jul 10 2020 at 04:33):

@Kyle Miller That looks perfect, thank you!

Mohammed Eyad Kurd-Misto (Jul 10 2020 at 04:35):

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

Last updated: Dec 20 2023 at 11:08 UTC