search

coq / coq-bench

Scripts for differential performance testing of Coq packages / versions
Other
4 stars 6 forks source link

Bench the coq installation too #89

Closed SkySkimmer closed 4 years ago

ejgallego commented 4 years ago

Umm, not sure this won't be misleading, IMO a misleading bench may be worse than no bench. I remain very very wary of measuring OCaml compilation time as simple refactorings can have a large impact on compilation time.

Actually we could improve the setup a bit already, by splitting the coq.opam packages into coq-base and coq-stdlib, then we could measure coq-stdlib.

SkySkimmer commented 4 years ago

Let's worry about that once the split is done.

ejgallego commented 4 years ago

Let's worry about that once the split is done.

OK; I'm still concerned about this bench, IMO it seems quite misleading and I'm worried that variations here will generate not very useful discussions, and in the end we will just ignore it.

But feel free to merge if you wanna have this.

p.s: Maybe we want to use a different development to test in Travis.

ppedrot commented 4 years ago

I personally prefer having a diff that is not reliable than no information, but YMMV.

SkySkimmer commented 4 years ago

If it's a problem we can always remove it.