On 08/12/10 16:47, Pierre Courtieu wrote:
Hi,
I answer Hendrik's message here because i did not recieve it.
Can you subscribe to the list Pierre? As a key developer it should be
obligatory!! 8-)
I'll send the earlier message to you which answers your last question to
me below, sorry forgot to CC you!
- D.
2010/12/8 David Aspinall<david.aspin...@ed.ac.uk>:
Quick followup to your second message:
- good idea to separate the two things, you can set up a customizable
command using % substitutions easily
- have you looked at the existing (surely broken, but not irreparable) code
for calling coqdep?
- D.
On 08/12/10 15:33, Hendrik Tews wrote:
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.
OK, I am getting your point.
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.
OK. I get your point completely now.
The idea is the following if I understand well.
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).
Tell me if I am wrong.
David, I am not sure coq-shell-insert-hook is the good entry point for
this kind of things. Is it?
Cheers,
Pierre
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
