Is this still broken?
probably yes, and probably not for you
actually, what do you mean by “broken”, or what do you want to? The current “fix” is that native_compute is disabled on Mac. Soon, it’ll be disabled by default for everybody who doesn’t opt-in. (See @Erik Martin-Dorel’s CEP).
The 10X slowdown was only confirmed for one user; smaller slowdowns were more common, IIRC especially with
with https://github.com/coq/ceps/pull/48 and its implementation, you should soon have the option to enable native by installing the
coq-native meta-package (and recompiling every coq library in your switch to produce its native version, so I advise a fresh opam switch)
Yes @Bas Spitters @Paolo Giarrusso, FYI the PR for
coq-native is now under review:
Very nice. BTW we'll want to do a computation that will take days when extracted to ocaml. What is the expected computation time in Coq. I seem to recall that we have mostly that one time compilation overhead, but I'm wondering whether there are more statistics available.
native compute is slower than the extracted code because it needs to handle strong reduction
Last updated: Jan 29 2023 at 08:28 UTC