Stream: Miscellaneous

Topic: native compute on mac


view this post on Zulip Bas Spitters (Nov 23 2020 at 08:38):

Is this still broken?
https://github.com/coq/coq/issues/11178

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 08:57):

probably yes, and probably not for you

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 08:09):

https://github.com/coq/coq/issues/8019


Last updated: Aug 19 2022 at 20:03 UTC