> 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.
Not particularly, this is to enforce the simplifying invariant that there is at
most only one buffer which can be partially processed. That in turn is to
simplify things for the user and for interaction with the proof assistant.
(As an aside: the PA side of the contract is the important one: the idea behind
PGIP was to turn this into a uniform protocol which could enable richer,
generic, user interfaces that *appear* to enable more elaborate interaction in
the UI but using the more restricted protocol behind the scenes with the
> 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.
Yes, of course, the use cases that you describe are very common and a common
complaint about working with PG -- partly because it forces this low-level view
of what is happening with the prover state abstraction directly in the UI.
> 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.
OK -- but the kill and restart is only happening now, because you have added
patches to make deactivating a scripting buffer kill the Coq process, right?
Is there a major drawback to killing and restarting in this case? Earlier you
said that loading compiled files was so cheap it didn't matter to redo this.
Is the issue that the UI loses this state (i.e. which files have been
processed)? Perhaps we need to cache the list of processed files and arrange
for them to be automatically required again (and locked in PG) on restart?
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.