In Proof General, the blue region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of atomic sequences of commands (ACS). Retraction is supported to the beginning of every ACS. By default, every command is an ACS. But the granularity of atomicity should be able to be adjusted.
This adjustment is essential when arbitrary retraction is not supported in the prover. Usually, after a theorem has been proved, one may only retract to the start of the goal. One needs to mark the proof of the theorem as an ACS. At present, support for these goal-save sequences has been hard wired. No other ACS are currently supported. We need a generalisation to overcome this deficiency.
This improvement should allow support for Coq's Section command, LEGO's Discharge and simplified support for Isabelle/Isar, by removing some of the prover-specific code.
References: Proof General manual (), and proof assistant manuals.
Skills: Good Emacs Lisp, understanding of "granularity" problem for proof assistant history mechanisms.
Proposer: David Aspinall (based on an original idea by Thomas Kleymann).