Extracting intermediate states

Stream: Is there code for X?

[Justin]

Is there a way to extract all the intermediate states of a theorem, like the state before/after a tactic or term?

[Gareth Ma]

What do you want the output to be like? How do you want to see the "states"

[Edward van de Meent]

do you know about mathlib's extract_goal tactic?

[Justin]

Gareth Ma said:

What do you want the output to be like? How do you want to see the "states"

Ideally pretty-printed like how the Tactic state looks like in the Lean interpreter, but also fine with anything that is machine readable. I want to create a dataset that includes the tactic/term, the before state, and the after state.

[Justin]

Edward van de Meent said:

do you know about mathlib's extract_goal tactic?

I know this is used to extract a subgoal as a theorem statement, but does this provide useful information beyond what is in the state?
Separately, is there a way to use extract_goal after the creation of every subgoal - can you put that in a script?

[Johan Commelin]

I think you might be interested in the tool that @David Renshaw recently developed, which can run a tactic at every goal step

[Kim Morrison]

Also see https://github.com/semorrison/lean-training-data for examples.

[David Renshaw]

https://github.com/dwrensha/tryAtEachStep is the thing I made, and I consulted
https://github.com/semorrison/lean-training-data/blob/master/TrainingData/InfoTree/Basic.lean and https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean for reference.

[Damiano Testa]

If you only want to print information about the states, a linter might be enough. You can look at the unreachable tactic linter for inspiration.

[Justin]

David Renshaw said:

https://github.com/dwrensha/tryAtEachStep is the thing I made, and I consulted
https://github.com/semorrison/lean-training-data/blob/master/TrainingData/InfoTree/Basic.lean and https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean for reference.

I noticed that one of your todos is making this work for terms. Is there more difficulty in extracting states after a term?