I was looking at the assembly code of Parray.set
. Indeed, this function computes Uint63.le Uint63.zero n
, which is true by definition. So, I was wondering if the OCaml compiler was able to optimize it away, or if we should just help the compiler by removing it. To my great surprise, not only is it not optimized, but the call to Uint63.le
is not even inlined. In fact, it is worth than that; it is not even a direct call, it is a full-blown closure invocation through caml_apply2
. So, what should have been a noop is actually a bitcoin-grade waste of computing resources.
For the record, here is Uint63.le
:
let le (x : int) (y : int) =
(x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
[@@ocaml.inline always]
So, are we using the attribute wrong? Or is it a bug in the OCaml compiler? Or is it a feature of Dune?
Ouch!
$ dune build _build/install/default/bin/coqtop.opt
File "kernel/parray.ml", line 122, characters 5-47:
122 | if (Uint63.le [@ocaml.inlined]) Uint63.zero n && Uint63.lt n l then
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error (warning 55 [inlining-impossible]): Cannot inline: Unknown function
Unknown function?
Do we pass -opaque
or whatever it's called?
Do you get the same thing if you build in "release" mode?
Indeed, it works in release mode.
But then, it begs the question, when we are doing benchs, are we doing them in release mode?
If benchs are based on the OPAM packages (coq-core.opam), those are built in release mode.
Where is the --profile=release
option passed?
dune build -p
implies release IIRC
-p PACKAGES, --for-release-of-packages=PACKAGES (required)
Shorthand for --release --only-packages PACKAGE.
from man dune build
and
--release
Put dune into a reproducible release mode. This is in fact a
shorthand for --root . --ignore-promoted-rules --no-config
--profile release --always-show-command-line
--promote-install-files --default-target @install
--require-dune-project-file.
Last updated: May 31 2023 at 15:01 UTC