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
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...
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.