2010/12/10 David Aspinall <david.aspin...@ed.ac.uk>: >> I don't want a solution based on proof-activate-scripting-hook, >> because I want to update files outside of emacs (eg by cvs >> update) while I am scripting in some buffer. > > But that's OK: the point of the "active" scripting buffer is to isolate the > one buffer that you are editing in the editor that *shouldn't* be > simultaneously changed outside your control in the file system.
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. Moreover as I said before: the set of ancestors may change during edition as user types its Require. > Emacs's own > hooks will check file-system consistency for you, with usual warning > messages and options to reload the buffer, etc. But you don't expect/want > this to happen when you've sent half of it Coq. > > When a new buffer becomes active, it is a chance to check that ancestor > files are compiled to their latest versions. For files that are compiled, > you might lock them inside PG to indicate this and that the user should not > edit them to become confused. If they do edit some file, then dependent > files will be unlocked automatically to indicate to the user that they need > recompiling to use updated ancestors. This feature is definitely what we want but it is an error to consider that dependecies are fixed, and that requred files are fixed. > See proof-included-files-list, doc here: > > http://bit.ly/dTItNV > > I think this could work nicely with Coq and compiled files. If you can try > out Isabelle, the trivial test cases include in etc/isar/multiple will > demonstrate how it works. Also look at the messages in the *isabelle* > buffer. > > I'm assuming it's not possible to invoke coqc from within coqtop? Instead, > you could use a cunning perl wrapper to multiplex the compile/proof commands > and use the existing PG configuration mechanisms. Your wrapper could even > spot "Require" commands and invoke "coqc" itself as you first thought of > doing with PG, then the messages issued could work with the existing > protocol. But that's maybe too kludgy, you would need to buffer commands, > etc. Interesting idea. No it is not possible for now. Problem: how coqtop would know which option (-I, -R etc) to give to coqc? P. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
