I like these 2 modes (novice and power user). It reflects the way people use
2011/1/17 Hendrik Tews <t...@os.inf.tu-dresden.de>
> 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?
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list