Thinking again on this:

> This optimisation becomes desirable because we have the situation with the 
> implementation that the control over ancestor files is fine-grained (i.e. 
> during scripting the file rather than at the start by parsing "imports" which 
> the included files behaviour assumed).  I think you made this decision for 
> implementation ease as well as accuracy, but  if you want now to 
> automatically retract things further than target region in certain cases, 
> that definitely looks like a Coq-specific function.

Actually, I realised that we do have the retraction behaviour you described for 
Isabelle already...

If the current Coq mechanism is using 
proof-register-possibly-new-processed-file, we could make the retraction 
operation you want generic, but we'd need to implement the span based mechanism 
(i.e. recording the included files in the Require-like span) in the generic 
code too.  

It doesn't seem worth doing this generically because, at least for Isabelle, we 
had already decided to put the dependency management in the prover.  Isabelle 
issues messages like "Proof General, you can unlock file XXX.thy" that are 
obeyed dumbly by PG.  So the span based mechanism would conflict/overlap with 

Another way to get the behaviour for Coq might have been to implement a wrapper 
around coqtop that spits out these messages at appropriate points, and hope 
that the Coq code could be patched at some point.

 - D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to