Ali Caglayan (Oct 16 2022 at 22:08): 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.
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?
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
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.
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.
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.
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
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 11:57):but we should name it properly
Pierre-Marie Pédrot (Oct 17 2022 at 11:59):we're testing the OCaml compiler way outside of its standard domain
Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):yes, but how is that useful for us?
Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):I mean to bench that
Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):for users it is irrelevant
Emilio Jesús Gallego Arias (Oct 17 2022 at 13:27):and moreover the testing we do means little
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 13:28):the bench seems like a waste of energy to me
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
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
Emilio Jesús Gallego Arias (Oct 17 2022 at 15:01):I guess we should ask them
Emilio Jesús Gallego Arias (Oct 17 2022 at 15:01):but that seems very brittle to me
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.
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: Apr 19 2024 at 20:01 UTC