| Age | Commit message (Collapse) | Author |
|---|
|
- Instead of the separate stage mechanism, we let make handle the
build and inclusion of all .d. Some initial calls to camlp4o
will fail, but make tries again later, and this finally works
great. These initial error message are made nice to avoid bad
interaction with M-x next-error
- The only recursive call to a sub-make is Makefile calling Makefile.build
in which the includes of .d take place. This allows to avoid compiling
anything for a make clean or make tags
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- We clarify their definition via some custom make function: find, diff...
- We avoid duplications via some $(sort ...)
- Some name changes:
* old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
.mly and .mll aren't in it anymore).
* new $(MLFILES) contains all .ml, either static or generated from
.mly .mll .ml4 or _mod.ml made out of .mllib
* $(ML4FILESML) is now $(GENML4FILES)
...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- This way, the Makefile.build gets shorter and simplier, with a few nasty
hacks removed.
- In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
This ways, *.cm* of .ml4 are correctly located, even when some .ml files
aren't generated yet.
- There is no risk of editing the .ml of a .ml4 by mistake, since it is by
default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
M-x next-error still open the right .ml4 at the right location.
- mltop.byteml is now mltop.ml, while mltop.optml keeps its name
- .ml of .ml4 are added to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- coq_makefile: utilise Coq_config pour avoir la liste des contribs
- mltop: normalisation des noms de modules ML (majuscule)
- Makefiles: introduction de fichiers %-mod.ml qui se chargent de faire
les declarations de modules ML d'un plugin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
build stages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* I encountered error messages during compilation, for instance
ocamlopt complaining about non-existing coq_config.cmi when compiling
coq_config.ml. Moreover, make was _not_ stopping at these errors
(WTF?!). After some debug, it turned out to be (indirectly) my fault:
I placed earlier the inclusion of the new .mllib.d in
Makefile.stage1, but this is too early, coqdep, which is used to
compute these files, isn't built yet. Due to the semantics of
"-include", make tries to build it, fails with the above error,
and goes on happily. Arrgh. After moving the inclusion of these
.mllib.d to Makefile.stage2, everything seems to work ok now.
* Since we're using such "nice" non-trivial features of make, I've
started a small FAQ section about them at the beginning of Makefile
* Recursive calls to make are now done with two options:
--no-builtin-rules : let's avoid builtin rules like "%:%.o" ...
--warn-undefined-variable : using a non-defined variable isn't
necessarily bad, but I found a few bugs with this option, and
I suggest we keep it.
* Clarified the rules about stage* in Makefile and their
STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_
have a chance to grasp in less than a day what's going on ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Documented in dev/doc/build-system.txt .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
