On 08/12/10 16:47, Pierre Courtieu wrote:

   > David, I am not sure coq-shell-insert-hook is the good entry point for
   > this kind of things. Is it?

I cannot find coq-shell-insert-hook. Did you mean

   > A command "Require f" is about to be sent to coq, but *before that* we
   > want to perform the following:
   >   1) send "Locate Library f"
   >   2) wait for the answer of coq: "path/to/f" .
   >   3) send "make -C ... path/to/f.vo"
   >   4) wait until make finished its job
   >   5) finally send the "Require f" to coq if everything went well (error
   > otherwise).

If it is not possible to communicate with the prover from within
proof-shell-insert-hook, then I consider the following approach:

- when commands are added to proof-action-list I insert a special
  command before every "Require" command. The special command is
  "Locate Library" with a special callback. 

- The special callback has the task to analyze the answer of coq
  to the "Locate Library" command and to start the recompilation

- This can only work if the following "Require" command is _not_
  sent to the prover before the special callback has finished its
  task. In order to achieve this one has to modify
  proof-shell-exec-loop, to run some callbacks before sending the
  next input to the prover.

The special commands that are inserted in proof-action-list do
not directly represent any source code. Therefore they probably
get an empty span. Will this cause any trouble?

I briefly looked at how callbacks are called: They get the span 
as argument, but not the prover output. The documentation says
that the prover output is available in the variable
proof-shell-last-output. Will this contain only the output from
the last command, or can it happen, that it contains the output
from, say, the last three commands?


ProofGeneral-devel mailing list

Reply via email to