@Janno and I wanted to add a new "control vernacular" (not sure about the name, I'm referring to stuff like
Succeed) via a plugin. In particular, is there an easy way to run a vernacular wrapped under such a new command from a plugin?
I don't think so
What is the "control" about?
"control" is what we call Time, Fail etc
in the code
I mean, which new control operator do you need, @Rodolphe Lepigre ?
We were gonna add something similar to
Time but that gives you an instruction count (using C bindings to the Linux perf API).
Ideally with an option to repeat the measurement several times to get a somewhat statistically significant result.
For example, we would like to do stuff like
Perf 10 Qed which would basically run
Succeed Qed 10 times, and print a report on instruction count usage at the end.
Last updated: May 28 2023 at 13:30 UTC