David Aspinall <david.aspin...@ed.ac.uk> writes: > 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. OK, I understand. For Coq however, if you modify an ancestor file, the complete locked ancestor is unlocked at once. So the invariant would not be broken if one does not change the active scripting buffer. In general, Coq's require commands can appear in the middle of a file. Say, for instance b.v requires a.v on line 100. Then, when you start changing a.v, you only have to undo b.v up to line 99. Then b.v could still be the only partially processed file, without breaking the invariant. In most of the Coq code that I saw until now, Require commands appear only at the beginning of the file, before all other material. So letting b.v remain a partially processed active scripting buffer (as described in the previous paragraph), would only be interesting, if the user organizes the Require commands as follows: (* First *) Require Some_big_and_expensive_to_load_and_rarely_changed_library. (* Second *) Require Everything_else. The idea here would be that if you change something in the ancestor hierarchy of Everything_else, the active scripting buffer is _not_ changed and the first line is _not_ undone. Then if you assert the second line again, you avoid loading the big library again. However, even the big libraries are loaded in about 1 second, so implementing this would only make sense if it doesn't require too much changes inside Proof General. > 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? Well, killing and restarting is the only correct solution for Coq. It will remain until it is possible to undo changes in the load path inside coqtop (which is currently not possible). There is a possible optimization to reuse the same Coq session if the load path and the working directory of the old and new active scripting buffer are identical. But I am unsure if it is worth implementing. Is there a major drawback to killing and restarting in this case? No, I just noticed this behavior and started to wonder... Earlier you said that loading compiled files was so cheap it didn't matter to redo this. Loading compiled files is cheap in comparison to reprocessing them from source. And usually it is even very fast, unless you load one of the big library packages, such as, for instance, the omega library for presburger arithmetic. Then loading takes about 1 second. Is the issue that the UI loses this state (i.e. which files have been processed)? No. I would even say the UI must clean this state. Because, when the user starts asserting again, Proof General must check the complete ancestor hierarchy in order to determine which files must be recompiled. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
