I would like to separate the following issues:

1. Detecting library loads inside ProofGeneral and finding out
   what file actually is meant

2. Deciding whether the library is up-to-date and performing the
   actions to make it up-to-date.

For issue 2 the simplest solution is to provide a user option for
an external command to be called. The command will contain some
keys that get substituted with file and directory. The default
would be something like "make -C %d %f.vo" resulting in 
"make -C some/dir foo.vo" if library foo in directory some/dir is

ProofGeneral should always provide this simplest solution,
because it scales to arbitrary projects with arbitrary

I would however also be interested to built some simple
dependency analysis into ProofGeneral, based on calling coqdep on
some .v files, analyzing the results and then possibly calling
coqc on some files. This would relieve simple projects from
providing a makefile.

However, in the emails before I only discussed issue 1. The
problem is that if library foo is required then you need to look
at coq's library path, in order to find out which files foo.v and
foo.vo are actually meant. It might be that there is foo.vo in
the current directory, but coq loads foo.vo from some other
directory or even complains that it cannot find foo.vo!

To solve issue 1 one can either model coq's library-finding
functionality inside ProofGeneral or ask coq with Locate Library.
The latter is simpler, but requires that one can synchronously
talk to coq without disturbing the rest of ProofGeneral.

Pierre Courtieu writes:
   On the other hand I don't really understand how you want to compute
   the set of files that need to be recompiled from within coq/emacs. Do
   you plan to look *recursively* into all files on which the current
   file depends? 

Sure, but this is a simple recursive function which does coqdep
before the recursive call and possibly coqc afterward. 

   This would have also the advantage that two different session of coq
   on two different files (one dependening on the other) would be

But there is no difference whether make or ProofGeneral calls

   Notice that this solution still needs a use of proof-shell-insert-hook
   but without sending something to the prover (but to make instead).
Only if you track library path modification commands. It would be
simpler to send Locate Library to find out which file needs to be

   Notice that this solution forces people to use coq_makefile, which is
   probably not a good idea.
If you have a user option for the external command with some keys
for the file and directory then people can plug their own
makefiles or even shell scripts.


ProofGeneral-devel mailing list

Reply via email to