2010/12/10 David Aspinall <david.aspin...@ed.ac.uk>:
> On 10/12/10 14:43, Pierre Courtieu wrote:
>> I agree with Hendrik, activate-scripting is not the right trigger
>> because dependencies may change *after* scripting is activated. Each
>> time the user adds "Require Import foo." and scripts it, proofgeneral
>> should try to compile foo.v if it is not up-to-date.
> This is actually pretty similar to what happens in Isabelle, it is just that
> Isabelle reports the dependencies to Proof General after it has processed
> the equivalent of Require  (and of course, it reads the file in on the heap
> at that point rather than compiling).

Reading the file on the fly (possible with the "Load" command) is not
correct to simulate a "Require" in coq because of name scopes (unless
we do something clever with modules). The "Load" command is not
equivalent to the "Require" command.

> So, if you don't want to parse the file first you can still use a new hook
> (or the kludgy wrapper idea, or a modified coqtop top level...) to issue the
> compile commands exactly when you process Requires,

I think this is exactly what Hendrik wants to do. The thing is: the
scripting should be paused until the compile command finishes. What is
the right way to do that?

>  but the rest of the
> active scripting mechanism could join up well.
>   (Note: when you undo a
> Require you should unlock the corresponding buffer too.)

Yes. There is one problem (already mentionned by Hendrik I think):
recursive dependencies are not capture this way. I don't think there
is a command to ask for it. I may implement (or advocate someone for)
a command which lists dependencies of a library.

> It would be great to get this working, but I am remembering why it wasn't so
> easy...

Actually I think Hendrik has found the right way to do it. We are almost there.
ProofGeneral-devel mailing list

Reply via email to