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?

Yes.

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:

  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.

 - 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