David Aspinall <david.aspin...@ed.ac.uk> writes:

   > 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.

So your answer is no? One cannot communicate with the prover from
inside proof-shell-insert-hook?

   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).

I am not going to implement something via some file-save hooks.
The simple reason is that anything based on file-save hooks is
not good enough for my personal working style. I often
synchronize with version control systems while the prover is
running, so files might change without emacs knowing it. 

   > 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).

There might be some misunderstanding: I want to use 
"Locate Library" only to map a library names to a file path. This
mapping depends on coq's LoadPath, which can be changed with
command line switches or with the various LoadPath commands at

Once I know which file gets loaded I have to compute its
dependencies in order to find out what has to get recompiled. For
this dependency checking one still has to use coqdep.

I also briefly looked at extracting dependencies from compiled
.vo files (which would be OK if the .vo file is up-to-date). The
checker coqchk is doing this, for instance, in order to build the
tree of all files to check. The .vo files contain a field with a
list of dependencies, but this field contains all dependencies,
not only the direct ones. However, for checking which .vo files
need recompilation one needs the direct dependencies. Moreover,
these dependencies are coq library path', not file names.


ProofGeneral-devel mailing list

Reply via email to