Stream: Coq devs & plugin devs

Topic: Missed inlining optimization

Guillaume Melquiond (Nov 24 2022 at 06:17):

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.

Guillaume Melquiond (Nov 24 2022 at 06:18):

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?

Maxime Dénès (Nov 24 2022 at 08:29):

Ouch!

Guillaume Melquiond (Nov 24 2022 at 08:37):

$ 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

Maxime Dénès (Nov 24 2022 at 08:38):

Unknown function?

Maxime Dénès (Nov 24 2022 at 08:38):

Do we pass -opaque or whatever it's called?

Maxime Dénès (Nov 24 2022 at 08:39):

Do you get the same thing if you build in "release" mode?

Guillaume Melquiond (Nov 24 2022 at 08:44):

Indeed, it works in release mode.

Guillaume Melquiond (Nov 24 2022 at 08:44):

But then, it begs the question, when we are doing benchs, are we doing them in release mode?

Pierre Roux (Nov 24 2022 at 08:49):

If benchs are based on the OPAM packages (coq-core.opam), those are built in release mode.

Guillaume Melquiond (Nov 24 2022 at 08:51):

Where is the --profile=release option passed?

Gaëtan Gilbert (Nov 24 2022 at 08:53):

dune build -p implies release IIRC

Gaëtan Gilbert (Nov 24 2022 at 08:54):

       -p PACKAGES, --for-release-of-packages=PACKAGES (required)
           Shorthand for --release --only-packages PACKAGE.

from man dune build

Gaëtan Gilbert (Nov 24 2022 at 08:54):

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: Dec 07 2023 at 09:01 UTC