Hi Hendrik
I looked at proof-shell-insert-hook. Is there a way to send a command to the prover, capture the output and retract this one command from within proof-shell-insert-hook? The documentation says that additional prompts will confuse proofgeneral. So is there a way to interact with the prover from within proof-shell-insert-hook without confusing proofgeneral?
Yes, the insert hook is intended to munge the string sent to the prover rather than insert extra commands at that point. You could add them to the queue, but that would be at the wrong moment.
The background is that coq has its own load path for libraries (where a library is a compiled .v file). To find out which file needs to be checked for recompilation it would be easiest to ask coq with the Locate Library command. But this would require a synchronous communication with coq from within proof-shell-insert-hook when an Require command is detected.
Or... you could do this at another time instead, for example, when the queue of commands is built, or when the file is loaded/saved using standard emacs hooks.
I think the file-load/save is a quite natural time to do this since it may interrupt the developer anyway and we try not to query the developer when sending commands in the background (so they can be looking at other parts of the script).
You'd lose when the user tries to process a Require command they've just typed but not saved the file, but you could issue a warning about this (or perhaps the require will fail anyway, in which case the user hits save-file and tries again).
Using Locate Library would have the advantage that proofgeneral does not need to model coq's library finding functionality.
That's *definitely* a good idea. (We tried to use coqdep for the auto-compile-vos option).
- 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.
