why does proof-retract-until-point make the current buffer the
active scripting buffer? It seems that Proof General anticipates
that the user starts asserting immediately afterward.

However, it might also be the case that the user does only make
some very small change and then goes to the previous active
scripting buffer (or to some other buffer) and continues
processing there. In this case the call to
proof-activate-scripting could have been saved. While for most
proof assistants the additional call to proof-activate-scripting
is probably not noticeable, for Coq it involves killing and
restarting the proof assistant. 

I am posting this because of the following: For Coq (and
probably other proof assistants as well) there are a number of
small changes that are processed in the following way. While
working in A you notice that such a small change is required in
B, which is a locked ancestor of A. So you change to B, unlock
it, make the small change and _immediately_ go back to A,
asserting to the point where you left. 

Examples for such small changes are:
- adding a simple definition
- changing an Import into an Export
- making an explicit argument implicit or vice versa.

In all these cases it is right to completely retract the current
scripting buffer A, because this ensures that the changes in B
are recompiled and loaded. However, it is not necessary to kill
and restart coqtop.


ProofGeneral-devel mailing list

Reply via email to