Undo

Harpoon includes an undo command to revert previous actions. Undo history is stored on a per-theorem basis, so ensure that the correct theorem is selected when executing undo. Only commands that effect a change to the subgoal list can be undone. Concretely, this means that Administrative tactics cannot be undone, since they do not introduce nor eliminate subgoals.

Harpoon also includes a command redo that will undo the effect of the last undo command. If a change to the subgoal list is effected, the redo history is purged. In other words, the history is stored linearly and no “undo tree” is available.

To see the state of the history, use the history command. This will show the history of commands that can be undone as well as whether any commands that can be redone.

Limitations

Undo cannot undo things such as creating new sessions. It also cannot undo the command that completes a proof, as beyond that point there is no more subgoal prompt through which the user could type undo.

Serializing the current Harpoon state will also cause the undo history to be lost. This is because serialization will cause Harpoon to reload all state from the signature. From Harpoon’s point of view, the list of subgoals it then has comes simply from the signature, not from a history of tactics.

To work around these limitations, we currently suggest manually undoing the offending actions by editing the proof script.