Hi, I like these 2 modes (novice and power user). It reflects the way people use coq nowadays. P.
2011/1/17 Hendrik Tews <[email protected]> > 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 >
_______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
