David Aspinall <david.aspin...@ed.ac.uk> writes:

   Instead of what you suggested, could we add an additional
   option to p-s-ro that would give you what you want? 

I only thought about a coq-specific solution that leaves the
other proof assistants untouched. Thinking about it, the feature
might also be interesting for other provers.

I would like to treat the locked material in the active scripting
buffer and those in ancestors in different ways. I prefer the
'retract setting for the active buffer. However, for ancestors I
would prefer being asked to choose one of the following:

1. Make scripting in ancestor ready. This is for the case that I
   want to continue with scripting in the ancestor. Proof General
   should retract up to the point where I can start scripting in
   the ancestor without being another question asked. For coq
   this means to completely retract the current active scripting

2. Make editing in ancestor possible. This is for the case that I
   only want to edit the ancestor and continue afterwards with
   scripting in the current active buffer. Moreover, I want to
   maintain consistency of my buffers and the prove assistant.
   For coq this means that the current scripting buffer must
   retract up to the appropriate Require command. When I change
   my mind and start scripting in the ancestor, then I am asked
   again, whether I would like to change the current scripting

3. Permit editing in the locked ancestor. This is for the case
   that I want to edit the ancestor without changing my current
   state in the active buffer. Thereby I accept the inconsistency
   between the buffer content and prover. For coq this means that
   only the span in the ancestor must be changed to read/write.
   When I switch to a different ancestor I want to have a new

For coq there is usually only a tiny difference between option 1
and 2, because Require commands are usually at the beginning of
the file. Therefore, I would be satisfied with a choice between 2
and 3 with the following optimisation for option 2: Proof General
must retract at least up to the Require that caused ancestor to
be locked. If there are only comments and Require commands above
this point then the current scripting should be retracted
completely. This way I can immediately start scripting in the
ancestor. If I instead go back to the (old) active buffer,
asserting those needlessly undone Require's is very fast.

Alternatively a choice between 1 and 3 would be fine, if there is
the following change for coq: If there is substantial material
above the Require that caused ancestor to be locked, then Proof
General should only retract up to this Require, but not the
material before it.

So in summary, I would like to see the following changes:

1. an additional option 'ask for proof-strict-read-only, which
   asks whether to retract or to permit modifications in the
   locked region.

2. splitting proof-strict-read-only into two variables, where one
   applies to the active buffer and the other applies to all
   other buffers.


ProofGeneral-devel mailing list

Reply via email to