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 runtime. 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
