Stream: Coq Platform devs & users

Topic: native_compute


view this post on Zulip Andrew Appel (Apr 14 2022 at 15:39):

On which platforms is native_compute enabled?
I have two different Coq-platform installations:
Coq 8.15.0 beta-package-pick for x86_32 Windows (32-bit)
Coq 8.15.0 beta-package-pick for x86_64 Ubuntu (64-bit), running under the WSL2 virtual machine.
In both of these, native_compute is not enabled, and it falls back to vm_compute.

view this post on Zulip Pierre Roux (Apr 14 2022 at 15:42):

In OPAM, there is a coq-native package (beware: installing it will recompile everything) but I don't think it's in any platform.

view this post on Zulip Michael Soegtrop (Apr 14 2022 at 16:43):

@Andrew Appel : In Coq Platform indeed native compute is not enabled on any platform to make things compatible. Since it is neither supported on Windows nor on macOS (where it works in principle but is quite a bit slower than vm_compute for most applications). I guess it would make sense to add a configuration question on this.

To enable it in Coq-platform, you would have to add a package coq-native to the package list (without version).

view this post on Zulip Andrew Appel (Apr 14 2022 at 17:08):

Thank you both for answering my questions. Who is the expert on native_compute who could answer my questions about how it works internally? What I'd like to know is, at what point does the code actually get compiled? Is it every time it runs?

view this post on Zulip Guillaume Melquiond (Apr 14 2022 at 17:09):

Definitions from imported libraries were compiled at the same time as those libraries. Definitions of the current file are compiled on the fly.

view this post on Zulip Karl Palmskog (Apr 14 2022 at 17:49):

maybe installing coq-native should be an explicit option in the Platform installation scripts (with a short explanation of what it means)? It would sure save time for people to do it upfront if they really need it

view this post on Zulip Michael Soegtrop (Apr 14 2022 at 17:57):

@Karl Palmskog Yes, that's what I meant with "I guess it would make sense to add a configuration question on this."

The main reason I didn't do this as yet is that I don't have much information on the native vs vm_compute milage on macOS. It is more or less hearsay that performance of native_compute on macOS is so bad that one shouldn't enable it unless one knows exactly what one is doing. So I don't really know what to recommend here.

It might also be an alternative to enable on Linux by default - as far as I know it does not have any disadvantages there.

@Guillaume Melquiond : I guess you have most experience with this. What is your advice?

view this post on Zulip Michael Soegtrop (Apr 14 2022 at 17:58):

We should also check if it does work on Windows with "compile from sources". In principle it should work.

view this post on Zulip Karl Palmskog (Apr 14 2022 at 17:59):

the main disadvantage I see is that there may be packages not compatible with native, so configuration option should come with some "caveat emptor": this is not tested, enable at own risk

view this post on Zulip Michael Soegtrop (Apr 14 2022 at 18:01):

I guess it is time to have an "expert mode" which enables more questions. I guess most users would be more annoyed by too many technical questions.

view this post on Zulip Michael Soegtrop (Apr 14 2022 at 18:02):

Anyway - before I enable it in Coq Platform, I would have to do solid testing, and I simply didn't have time for this as yet. Help with that would be very welcome.

view this post on Zulip Karl Palmskog (Apr 14 2022 at 18:04):

unfortunately we don't even do testing of native in the opam archive (https://github.com/coq/opam-coq-archive/issues/1498)

view this post on Zulip Guillaume Melquiond (Apr 14 2022 at 18:23):

Michael Soegtrop said:

I guess you have most experience with this. What is your advice?

I am all for making it easier to enable. But even on Linux, I would not enable by default, as there are quite a few libraries that cause the OCaml compiler to overflow its stack. (Nothing that cannot be fixed with ulimit -s, but still, that is hardly an enjoyable user experience.)

view this post on Zulip Enrico Tassi (Apr 15 2022 at 09:35):

Actually https://github.com/coq/opam-coq-archive/pull/1504 is stuck because I couln not find a package failing

view this post on Zulip Maxime Dénès (Apr 15 2022 at 13:00):

IIRC, the only problem with native_compute on Windows used to be limitations on the size of command arguments. But ocamlopt now has a -args argument to read them from a file. @Michael Soegtrop are there other windows-related problems you are aware of, for native compute ?

view this post on Zulip Michael Soegtrop (Apr 15 2022 at 17:39):

I guess I should just try what happens on Windows.

view this post on Zulip Michael Soegtrop (Apr 15 2022 at 17:40):

@Guillaume Melquiond : can you recommend a few tough test cases?

view this post on Zulip Guillaume Melquiond (Apr 16 2022 at 06:44):

Michael Soegtrop said:

can you recommend a few tough test cases?

For example, Interval does not compile to native code with the default settings on Linux. (At least with OCaml 4.13.1. That might obviously depend on the version of the compiler.)


Last updated: Jan 30 2023 at 10:03 UTC