On 10/12/10 11:43, Hendrik Tews wrote:
David Aspinall<david.aspin...@ed.ac.uk> writes:
Did you consider the scripting time option, file activated for
scripting? This is the place that saves of potential-ancestor files
What precisely do you mean? Do you mean ProofGeneral's concept of
the active scripting buffer and proof-activate-scripting-hook?
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. 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.
See proof-included-files-list, doc here:
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
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.
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.