Hi, 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 required. ProofGeneral should always provide this simplest solution, because it scales to arbitrary projects with arbitrary dependencies. 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 facilitated. But there is no difference whether make or ProofGeneral calls coqc. 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 rebuild. 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
