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.
In OPAM, there is a
coq-native package (beware: installing it will recompile everything) but I don't think it's in any platform.
@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).
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?
Definitions from imported libraries were compiled at the same time as those libraries. Definitions of the current file are compiled on the fly.
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
@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?
We should also check if it does work on Windows with "compile from sources". In principle it should work.
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
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.
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.
unfortunately we don't even do testing of native in the opam archive (https://github.com/coq/opam-coq-archive/issues/1498)
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.)
Actually https://github.com/coq/opam-coq-archive/pull/1504 is stuck because I couln not find a package failing
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 ?
I guess I should just try what happens on Windows.
@Guillaume Melquiond : can you recommend a few tough test cases?
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