|
|
Sequel to commit 14476 : in fact, even with "tools" in .PHONY,
we still may have coqdep stuff being recompiled in a "make"
that follows a successful "make". This seems to related to
the hacks I've introduced to prevent ocamlopt from erasing
and recreating .cmi when there's no .mli around
(cf. comment around line 823 in Makefile.build).
Scenario:
- First we build coqdep_boot directly out of coqdep_lexer.ml and co.
When ocamlopt is around, this creates some .cmx and .cmi,
but no .cmo.
- Later we build coqdep, which need coqdep_lexer.cmx and co.
Now "make" checks whether these .cmx are up-to-date.
But our hacks made these .cmx depend on the corresponding .cmi.
Then "make" checks whether these .cmi are up-to-date.
But our hacks made these .cmi depend on the corresponding .cmo.
These .cmo doesn't exist yet, we run ocamlc, which recreates
the .cmi with same content but a different timestamp.
For some strange reason, even with refreshed .cmi, the .cmx
are not remade by this run, but will be on the next run.
Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi
should be improved, but I see currently no simple solution.
In the meantime, an simple ad-hoc fix is to create these two .mli ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre Boutillier
letouzey
herbelin