Shrink

[dselsam]

Strip unused have statements (and their proofs) from proofs. Note: only lightly tested.

[spolu]

@dselsam Thinking more about using that for real. We'll need the sequence of tactic state on top of the sequence of tactics to be able to fully reconstruct the data we need.

Any chance this is easy to add?

[dselsam]

@dselsam Thinking more about using that for real. We'll need the sequence of tactic state on top of the sequence of tactics to be able to fully reconstruct the data we need.

Any chance this is easy to add?

@spolu Sure, I am literally throwing out this information at the very end: https://github.com/dselsam/lean3-gym/blob/shrink/src/repl.lean#L334 What format do you want specifically? The representation I am using ([(ts1, action, ts2)]) duplicates the tactic-states, which is fine with reference-counting but bad when converting to string.

[spolu]

I think we can simply do [(TacticState, Tactic)] and have as a convention that the last TacticState (omitted) is assumed to be no goals?

[spolu]

This all looks great \o/

Two comments before merge:

• Shouldn't we run validate_proof in try_finish?
• I think we want to update the README with the new API