| Age | Commit message (Collapse) | Author |
|---|
|
We're back to a unique build phase (as before e372b72), but without
relying on the awkward include-deps-failed-lets-retry feature of make.
Since PMP has made grammar/ self-contained, we could now build
grammar.cma in a rather straightforward way, no need for
a specific sub-call to $(MAKE) for that. The dependencies between
files of grammar/ are stated explicitely, since .d files aren't
fully available initially.
Some Makefile simplifications, for instance remove the CAMLP4DEPS
shell horror. Instead, we generalize the use of two different
filename extensions :
- a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp)
- a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo),
except coqide_main.ml4 and its specific rule
Note that we do not generate .ml4.d anymore (thanks to the .mlp vs.
.ml4 dichotomy)
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If you want to try, it should be now as simple as:
make clean && ./configure -local -usecamlp4 && make
For the moment, the default stays camlp5, hence
./configure -usecamlp5 and ./configure are equivalent.
Thanks to a suggestion by N. Pouillard, the remaining
incompatibilities are now handled via some token filtering in
camlp4. See compat5*.mlp. Morally, these files should be named .ml4,
but I prefer having them not in $(...ML4) variables, it might confuse
the Makefile... The empty compat5*.ml are used to build empty .cmo
for making camlp5 happy. For camlp4,
- tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
- tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
syntax such that VERNAC EXTEND, we only load it for a few files via
camlp4deps
TODO: check that my quick adaptation of camlp5-specific code in
tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur
is hiding information in the locations ?!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
|
