diff options
| author | Guillaume Melquiond | 2015-04-27 12:07:36 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-04-27 12:07:36 +0200 |
| commit | 2887393cf817d0509caf7a2bb8f7850e2bc2d123 (patch) | |
| tree | 500702d407e82817bda79b746007014b4b319998 | |
| parent | 62b0708ebfda01e377c4e6e229be4388a96cbecc (diff) | |
Compile the VM code with some optimizations (+130% speedup).
Option -g has no impact on the code generated by GCC, so it is now
systematically added, since it is quite helpful when the VM segfaults
(e.g. bug #4203). Note that, even for a debug build, option -O1 is
preferred to -O0, since -O0 produces assembly code that is much too noisy
for debugging.
For non-debugging builds, -O2 was chosen rather than -O3, since it led to
a noticeably faster VM. I guess even recent GCC compilers still have a
hard time optimizing humongous functions such as the VM.
Here are the results on a simple benchmark: computing the factorial of a
large number with Z and BigZ. (Factorial of 2*6! for Z, of 7! for BigZ.)
For comparison purpose, the timings of native_compute are also provided.
Z BigZ
-O0 6.4 12.3
-O1 4.3 10.7
-O2 2.8 7.3
-O3 3.0 9.3
n_c 2.0 2.4
| -rw-r--r-- | configure.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/configure.ml b/configure.ml index 92d71813c1..68fe7e1211 100644 --- a/configure.ml +++ b/configure.ml @@ -396,8 +396,7 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes" else "" -let cflags = "-Wall -Wno-unused" - +let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2") (** * Architecture *) |
