David Aspinall writes:
Date: Wed, 12 Jan 2011 12:38:17 +0000
Subject: Multiple files: coq-process-require-command
I reply to ProofGeneral-devel, because I hope Pierre will share
his opinion on these issues.
Do you plan to support coq-process-require-command to handle your last
but one bullet point missing feature? ("Sources of required modules are
not locked inside Proof General.")
To integrate with the existing management it might work to call
proof-register-possibly-new-processed-file here on some list of files.
Indeed, one could place a call to
proof-register-possibly-new-processed-file inside
coq-make-lib-up-to-date. This would lock all ancestors that are
processed in internal recompilation mode. (
However, I am not satisfied with what happens when I switch to
one of these looked ancestors. What currently happens is that
when I start typing there, I am forced to completely retract the
current buffer. IMO this is too much for coq.
For coq I see two possible reactions when the user starts typing
in a locked ancestor:
1 - for novices who don't know their dependencies:
Retract the current scripting buffer up to the point before the
Require command that establishes the ancestor dependency. There
might be material before this Require command, which does not
depend on the ancestor.
If the changes are simple, the user might not want to do any
scripting in the ancestor buffer. After the changes, he might
want to go directly back and process the Require again, thereby
causing a recompilation of the ancestor.
For the implementation: In internal mode it is easy to store
the complete set of ancestors somewhere, for instance as a
property of the span of the Require command. Then when an
ancestor is changed, one only has to search for this ancestor
in the spans of the current scripting buffer.
2 - for power users who know their dependencies:
Simply unlock the buffer without doing any changes to the
current scripting buffer. Of course, this way the changes in
the ancestor will not be visible in the current scripting
buffer. The power user knows this and if he wants to get the
changes he does the necessary retracting himself.
This behaviour makes sense when you are deep inside some proof
development and you notice that for the current goal you need
some additional Lemma in some ancestor. You don't want to check
all this immediately, because you expect much more lemmas to be
missing. So you postpone the current goal, add the lemma
without proof to the ancestor and continue the proof with the
next open goal. Once you finished, you go to all ancestors,
proof all the new lemmas and come then back to the original
theorem to finish all the postponed goals.
There should probably a user option with three possible values:
- always-retract gives 1
- ask requests the user to choose between 1 and 2
- never-retract gives 2
How can I achieve 1 and 2?
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
