Andrew Appel (Apr 14 2022 at 15:39): 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.
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.
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).
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?
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.
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
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?
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.
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
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.
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.
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)
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.)
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
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 ?
Michael Soegtrop (Apr 15 2022 at 17:39):I guess I should just try what happens on Windows.
Michael Soegtrop (Apr 15 2022 at 17:40):@Guillaume Melquiond : can you recommend a few tough test cases?
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: Jun 03 2023 at 05:01 UTC