aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-27 12:07:36 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-27 12:07:36 +0200
commit2887393cf817d0509caf7a2bb8f7850e2bc2d123 (patch)
tree500702d407e82817bda79b746007014b4b319998 /ide/coq.lang
parent62b0708ebfda01e377c4e6e229be4388a96cbecc (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
Diffstat (limited to 'ide/coq.lang')
0 files changed, 0 insertions, 0 deletions