I like these 2 modes (novice and power user). It reflects the way people use
coq nowadays.

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?
> Bye,
> Hendrik
> _______________________________________________
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
ProofGeneral-devel mailing list

Reply via email to