Bas Spitters (Nov 23 2020 at 08:38): Bas Spitters (Nov 23 2020 at 08:38):Is this still broken?
https://github.com/coq/coq/issues/11178
Paolo Giarrusso (Nov 23 2020 at 08:57):probably yes, and probably not for you
Paolo Giarrusso (Nov 23 2020 at 08:59):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).
Paolo Giarrusso (Nov 23 2020 at 09:00):The 10X slowdown was only confirmed for one user; smaller slowdowns were more common, IIRC especially with flambda
Paolo Giarrusso (Nov 23 2020 at 09:02):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)
Erik Martin-Dorel (Nov 23 2020 at 22:58):Yes @Bas Spitters @Paolo Giarrusso, FYI the PR for coq-native is now under review:
https://github.com/ocaml/opam-repository/pull/17690
Bas Spitters (Nov 24 2020 at 07:50):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.
Pierre-Marie Pédrot (Nov 24 2020 at 08:09):native compute is slower than the extracted code because it needs to handle strong reduction
Pierre-Marie Pédrot (Nov 24 2020 at 08:09):https://github.com/coq/coq/issues/8019
Last updated: May 31 2023 at 03:30 UTC