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

Reply via email to