| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
* Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
* As a consequence, we enrich this Coq_config with stuff that was
only in config/Makefile
* replace the big ugly find by some dependencies against source files
* by the way: build csdpcert, with the right aliases.
I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Dealing with .vo files was harder than anticipated (issues with
coqdep_boot and the location of the .v files). Current solution
cannot compete for a beauty prize, but well.
Several other issues remain (see top and bottom of myocamlbuild.ml)
- For the moment the coqlib / coqsrc in Coq_config is to be
hacked by hand to add _build/ in it.
- Parallelism is a "no go" for the moment. Ocamlbuild accepts
a -j option, but it has almost no effect experimentally.
(but at least it doesn't take more time than make -j1,
i.e. about 14 min here, instead of about 7 for make -j2)
- After a first full build, ocamlbuild is awfully slow
to detect that nothing has to be redone (1 min 25 here)
To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
* a small shell script ./build to drive ocamlbuild
* rules for all the binaries (apart from coqide and coqchk)
* use of ocamlbuild's Echo instead of using shell + sed + awk
for generated files
* Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
list of things to "clean"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 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
|
letouzey