| Age | Commit message (Collapse) | Author |
|
* 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
|
|
* In eval_cone and simpl_cone, default patterns were leading
to duplicated computations. Adaptation of RingMicromega.v
to prevent that.
* Use the Ocaml builtin types (lists, pairs, bool, etc) and
remove the useless conversion functions in mutils.ml and alii.
* andb was extracted to a correctly lazy but ugly match.
Let's rather use Ocaml's (&&).
Remain to be done: take advantage of extraction during the build,
- either directly if we are using plugins, (no dependency issues)
- or if we compile statically, at least check later that the
micromega.ml in the archive and the one auto-generated are in sync.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12034 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
|