Stream: coqbot devs & users

Topic: @coqbot bench native


view this post on Zulip Ali Caglayan (Oct 16 2022 at 22:08):

I've added a new command to coqbot which together with #16679 will allow you to write

@coqbot bench native

to start a bench with coq-native enabled.

view this post on Zulip Pierre-Marie Pédrot (Oct 17 2022 at 06:26):

Great! No more fiddling with dummy patches! A question, though: does it display the fact that native was enabled in the coqbot summary message?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 10:46):

Why do we care about testing this? To me, it seems mostly a large waste of cycles

view this post on Zulip Pierre-Marie Pédrot (Oct 17 2022 at 11:26):

Because as long as native exists, we want to be sure it is not completely broken.

view this post on Zulip Ali Caglayan (Oct 17 2022 at 11:43):

Pierre-Marie Pédrot said:

Great! No more fiddling with dummy patches! A question, though: does it display the fact that native was enabled in the coqbot summary message?

No, but I could do that.

view this post on Zulip Ali Caglayan (Oct 17 2022 at 11:44):

Emilio Jesús Gallego Arias said:

Why do we care about testing this? To me, it seems mostly a large waste of cycles

If we don't have this feature, people will still bench native, it is just a convencience.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:57):

Pierre-Marie Pédrot said:

Because as long as native exists, we want to be sure it is not completely broken.

how does the bench help with that? I was under the impression that was the role of CI

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:57):

I'm happy if we want to test the performance of the OCaml compiler

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 11:57):

but we should name it properly

view this post on Zulip Pierre-Marie Pédrot (Oct 17 2022 at 11:59):

we're testing the OCaml compiler way outside of its standard domain

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):

yes, but how is that useful for us?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):

I mean to bench that

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):

for users it is irrelevant

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):

and moreover the testing we do means little

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):

it could be that one OCaml version works Ok, some other could just give totally different bench numbers

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 13:28):

the bench seems like a waste of energy to me

view this post on Zulip Gaëtan Gilbert (Oct 17 2022 at 13:48):

Emilio Jesús Gallego Arias said:

for users it is irrelevant

how is it irrelevant? IMO users don't care if the time is spent in coqc itself or in a child ocamlopt

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 15:00):

Native users will care how fast the native conversion is, not OCaml compiling their code

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 15:01):

I guess we should ask them

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2022 at 15:01):

but that seems very brittle to me

view this post on Zulip Ali Caglayan (Oct 17 2022 at 17:09):

As it stands, we don't have a native bench per say. However the code we generate that gets compiled by ocamlopt still needs to be benched. When we are playing around with how the term gets translated, we want to see if it makes the compiler slower etc.

view this post on Zulip Maxime Dénès (Jan 23 2023 at 21:03):

Native compilation is a bit like a JIT. Users care about the sum of compilation time and running time, because both can occur when testing for convertibility.


Last updated: Jan 31 2023 at 10:01 UTC