> 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 
prover) 

> 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?

 - D.

_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to