Rodolphe Lepigre (Jun 27 2023 at 11:20): Rodolphe Lepigre (Jun 27 2023 at 11:20):I recently submitted a PR that provides a new vernacular command, as well as new command-line options (similar to -time and -time-file), that let one get CPU instruction counts for individual commands (on Linux). To us, this extension would be extremely valuable as we are always looking out for performance regressions. (We already have a setup that gives us such data per file, but that is too coarse-grained.)
One issue with this PR, that was raised by @Gaëtan Gilbert, is that it is not great to add yet another set of command-line flags that do a similar thing to -time and -time-instr, and it would be better to combine these somehow. While I fully agree with this point, I would like to understand how much of a blocker this is (we are kind of hoping this PR still can make it in 8.18.0, since we really need this feature). To us, removing the command-line flags is not an option, because the whole point of the MR is to collect data as part of CI runs.
Rodolphe Lepigre (Jun 27 2023 at 11:20):Personally, I don't think adding such command line flags is such a big deal, even if they are added with the understanding that they are just a temporary solution while we figure out how to properly collect performance data into a single, machine-readable format (like Gaëtan is trying to do here).
Gaëtan Gilbert (Jun 27 2023 at 11:37):https://github.com/coq/coq/pull/17702 is IMO ready so we could just merge it then add instruction counts to it
Théo Zimmermann (Jun 27 2023 at 11:42):Rodolphe Lepigre said:
Personally, I don't think adding such command line flags is such a big deal, even if they are added with the understanding that they are just a temporary solution while we figure out how to properly collect performance data into a single, machine-readable format (like Gaëtan is trying to do here).
Merging and releasing a feature "with the understanding that they are just a temporary solution" is never valid. If it gets released in Coq, it won't be temporary and will have to be maintained. Isn't it an option to provide this command-line from a plugin?
Karl Palmskog (Jun 27 2023 at 11:49):From the user side, indeed people tend to start to depend on these kinds of features, and there might be issues about documenting them, etc.
With Coq plugins, you will likely never have those problems.
Janno (Jun 27 2023 at 11:51):How can plugins interact with command line options? IIRC not even options provided by plugins can be turned on via command line because the plugin probably won't be loaded before -set is interpreted.
Rodolphe Lepigre (Jun 27 2023 at 12:16):Théo Zimmermann said:
Merging and releasing a feature "with the understanding that they are just a temporary solution" is never valid. If it gets released in Coq, it won't be temporary and will have to be maintained.
I don't see why Coq could not expose some features with an unstable API, as long as they are documented as such.
Théo Zimmermann (Jun 27 2023 at 12:18):Rodolphe Lepigre said:
Théo Zimmermann said:
Merging and releasing a feature "with the understanding that they are just a temporary solution" is never valid. If it gets released in Coq, it won't be temporary and will have to be maintained.
I don't see why Coq could not expose some features with an unstable API, as long as they are documented as such.
There are tons of supposedly experimental features in Coq that people heavily depend on.
Rodolphe Lepigre (Jun 27 2023 at 12:19):Gaëtan Gilbert said:
https://github.com/coq/coq/pull/17702 is IMO ready so we could just merge it then add instruction counts to it
Oh OK, that did not seem ready to me, but I only had a quick look.
Last updated: Nov 29 2023 at 22:01 UTC