@Janno and I wanted to add a new "control vernacular" (not sure about the name, I'm referring to stuff like Time
or 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
You can't.
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: Dec 05 2023 at 04:01 UTC