Yes but files on which it depends may have changed by cvs (typically
you cvs update an external library to its current version). When will
this be detected? It would be tedious to have to deactivate/reactivate
scripting to detect this. Going back to the require and forward should
be enough.


This is confusing... I think you're asking for something that neither mechanism we've talked about is trying to do. I don't mean that you turn on/off scripting every time you type a Require command, although we could argue about how bad that really would be (aren't Require commands almost always collected at the top of the file?).

I'm suggesting Hendrik uses the existing included files mechanism *and* the coqc/LoadPaths triggers, to give better user feedback on the status of files up-to-date/not in the interface. This was the point of the original included files design. So files which have been compiled are considered up-to-date and are locked. The locking happens when the Require is processed, which is what you want, and up-to-date checks could be made here (IIRC the locking is simplistic: it locks an already visited buffer, and arranges that if that file is visited in future it will be locked).

You can always subvert the interface locking if you want to, explicitly with the options, or behind the scenes by being naughty. The point is to have a simple mechanism that gives the user some useful hints in most cases. Personally, I would think that running a big cvs update in the middle of scripting a complex file that depends on the libraries you're updating is not a sensible idea!!

Moreover as I said before: the set of ancestors may change during
edition as user types its Require.
....
This feature is definitely what we want but it is an error to consider
that dependecies are fixed, and that requred files are fixed.

This is straightforward, you need to tell PG the dependencies but you can do this from seeing the Require (exact single dependency), or from the output it produces (recursively included files as well). Same as in Isabelle, you should really take a look at it...

 - D.
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

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

Reply via email to