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

   Is there a major drawback to killing and restarting in this

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.


ProofGeneral-devel mailing list

Reply via email to