You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 4935 Reporter: letouzey Status: closed (set by @gasche on 2016-02-16T00:24:19Z) Resolution: suspended Priority: normal Severity: feature Version: 3.11.1 Category: -for ocamlbuild use https://github.com/ocaml/ocamlbuild/issues Related to:#5138 Monitored by:@ygrek "Julien Signoles" @hcarty
Bug description
I'm trying to compile Coq via ocamlbuild (See also bug #4934). Currently, the use of the -j option brings almost no time gain on a multi-core machine (while make -j is close to 2x gain on dual-core and 3.5x gain on quad-core).
Here again, I may well be the culprit and not have written my myocamlbuild.ml in an appropriate manner. Any hint is welcome...
Best regards,
Pierre Letouzey
Instructions to reproduce:
you'll need camlp5 installed
get a copy of coq development archive
svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk/ [^]
./configure -local -opt
Launch a first build (./build is a wrapper for ocamlbuild, with no -j) :
./build
Redo the same with -j 0 :
rm -rf _build
ocamlbuild -j 0 coq.otarget
Here, on a quad-core machine, first build says:
Finished, 2716 targets (0 cached) in 00:13:10.
While the second one says
Finished, 2716 targets (0 cached) in 00:12:37.
On the same machine, make -j perform the same build in about 4min.
The text was updated successfully, but these errors were encountered:
Original bug ID: 4935
Reporter: letouzey
Status: closed (set by @gasche on 2016-02-16T00:24:19Z)
Resolution: suspended
Priority: normal
Severity: feature
Version: 3.11.1
Category: -for ocamlbuild use https://github.com/ocaml/ocamlbuild/issues
Related to: #5138
Monitored by: @ygrek "Julien Signoles" @hcarty
Bug description
I'm trying to compile Coq via ocamlbuild (See also bug #4934). Currently, the use of the -j option brings almost no time gain on a multi-core machine (while make -j is close to 2x gain on dual-core and 3.5x gain on quad-core).
Here again, I may well be the culprit and not have written my myocamlbuild.ml in an appropriate manner. Any hint is welcome...
Best regards,
Pierre Letouzey
Instructions to reproduce:
svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk/ [^]
./build
rm -rf _build
ocamlbuild -j 0 coq.otarget
Here, on a quad-core machine, first build says:
Finished, 2716 targets (0 cached) in 00:13:10.
While the second one says
Finished, 2716 targets (0 cached) in 00:12:37.
On the same machine, make -j perform the same build in about 4min.
The text was updated successfully, but these errors were encountered: