Hi Hendrik

Thanks for looking at this! Pierre and I had investigated a few ideas, you can still see some code remains in coq.el from some old attempts that partly worked (auto-compile-vos), but it seemed that Coq users were never hugely interested in the feature.

There is some code to take action after a require has been processed, but, as you say, maybe something should be done just before as well to check compiled files are up to date. I'm not sure whether the file save/load hooks would be more appropriate than a hook run when command is queued, or whether connecting to standard Emacs make mechanisms would be sensible. For your way, maybe the standard proof-shell-insert-hook would work? This runs when a command is actually sent to the process, versus when it is queued.

Anyway, would be very happy to get this working with latest Coq and accept a patch. Maybe discussing further on our Trac would be best, there is this ticket here:


Best wishes,

- David

On 06/12/10 12:13, Hendrik Tews wrote:

After looking a bit at the code, I believe it is best to install
a new hook, say proof-enqueue-item-hook, that is called in
proof-add-to-queue just before the queueitems are appended to the
proof-action-list. The hook would be called for every item in

coq-mode can then install a function in the hook that looks for
require commands and takes appropriate actions. The hook variable
itself should be buffer local, to avoid that the
coq-require-filter function is called in an Isabelle session.

Any comments?


ProofGeneral-devel mailing list

ProofGeneral-devel mailing list

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

Reply via email to