Stream: Coq devs & plugin devs

Topic: Adding a new control vernacular using a plugin


view this post on Zulip Rodolphe Lepigre (Nov 24 2022 at 13:37):

@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?

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 14:28):

I don't think so

view this post on Zulip Enrico Tassi (Nov 24 2022 at 14:39):

You can't.
What is the "control" about?

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 14:45):

"control" is what we call Time, Fail etc

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 14:45):

in the code

view this post on Zulip Enrico Tassi (Nov 24 2022 at 14:57):

I mean, which new control operator do you need, @Rodolphe Lepigre ?

view this post on Zulip Rodolphe Lepigre (Nov 24 2022 at 15:33):

We were gonna add something similar to Time but that gives you an instruction count (using C bindings to the Linux perf API).

view this post on Zulip Rodolphe Lepigre (Nov 24 2022 at 15:33):

Ideally with an option to repeat the measurement several times to get a somewhat statistically significant result.

view this post on Zulip Rodolphe Lepigre (Nov 24 2022 at 15:35):

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: Feb 01 2023 at 15:04 UTC