Is this still broken?
https://github.com/coq/coq/issues/11178
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 flambda
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:
https://github.com/ocaml/opam-repository/pull/17690
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
https://github.com/coq/coq/issues/8019
Last updated: Dec 06 2023 at 14:01 UTC