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
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?
$ 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
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
--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