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?

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.

Using Locate Library would have the advantage that proofgeneral
does not need to model coq's library finding functionality.


ProofGeneral-devel mailing list

Reply via email to