diff options
| author | Emilio Jesus Gallego Arias | 2019-02-28 00:12:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-21 13:02:19 +0200 |
| commit | 4a60c81e9fc67d98558b48d9f79e2d3610d60d77 (patch) | |
| tree | bb3a21ec0911f87e8ffa9086a6482c67a65e41d0 | |
| parent | 623a431c293dcff42b4bc4dc3dc50c047a9ecbcc (diff) | |
[dune] Enable optimization options in the compilation of the VM.
So far we didn't setup optimization flags for the VM in the Dune
build, but time has come to experiment with such flags, we try -O3.
Enabling `-flto` in the final binary build would be great, however
this seems to break windows.
| -rw-r--r-- | dune | 7 | ||||
| -rw-r--r-- | topbin/dune | 2 |
2 files changed, 9 insertions, 0 deletions
@@ -8,6 +8,13 @@ (ocaml409 (flags :standard -strict-sequence -strict-formats -keep-locs -rectypes -w -9-27+40+60 -warn-error -5 -alert --deprecated))) +; Information about flags for release mode: +; +; In #9665 we tried to add (c_flags -O3) to the release setup, +; unfortunately the resulting VM seems to be slower [5% slower on +; fourcolor, thus we keep the default C flags for now, which seem to +; be -O2. + ; The _ profile could help factoring the above, however it doesn't ; seem to work like we'd expect/like: ; diff --git a/topbin/dune b/topbin/dune index 3b861afe78..7b77826216 100644 --- a/topbin/dune +++ b/topbin/dune @@ -26,6 +26,8 @@ (package coq) (modules coqc_bin) (libraries coq.toplevel) + ; Adding -ccopt -flto to links options could be interesting, however, + ; it doesn't work on Windows (link_flags -linkall)) (install |
