Stream: Coq devs & plugin devs

Topic: Bench for native compute


view this post on Zulip Pierre-Marie Pédrot (Apr 28 2022 at 16:55):

This message is trying to attract the attention of people who happen to be users of the native compilation mechanism, but haven't seen the discussion going on in https://github.com/coq/coq/pull/15944.

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2022 at 16:55):

I am looking for a reasonable set of developments which could be used as a benchmark of said mechanism.

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2022 at 16:57):

Not only would I like to push this PR forward, but I've got a few more stuff I'd like to test, notably the newly available -linscan option after the bump to OCaml >= 4.09

view this post on Zulip Karl Palmskog (Apr 28 2022 at 18:30):

is OCaml 4.05.0 finally getting dropped? :tada:

view this post on Zulip Pierre-Marie Pédrot (Apr 28 2022 at 18:49):

Yes, we're now requiring OCaml >= 4.09

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 18:59):

:broken_heart: no 4.07.1 :-(

view this post on Zulip Paolo Giarrusso (Apr 28 2022 at 18:59):

Look forward to testing 4.09 with the GC patch

view this post on Zulip Ali Caglayan (May 18 2022 at 13:54):

I noticed @Maxime Dénès has a little suite here: https://github.com/maximedenes/native-compute-bench

view this post on Zulip Maxime Dénès (May 18 2022 at 13:59):

Ah ah, I had completely forgotten this existed. Thanks :)

view this post on Zulip Maxime Dénès (May 18 2022 at 14:00):

These two examples are probably not sufficient, but it would be nice indeed to run them on @Pierre-Marie Pédrot 's branch

view this post on Zulip Maxime Dénès (May 18 2022 at 14:00):

They can at least detect some issues


Last updated: Feb 06 2023 at 19:03 UTC