> 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 [email protected] 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.
