I would like to benchmark how long a declaration takes to compile. Are there built-in tools for doing so?
So far the best I have come up with is to write an external script that produces a .v
file with a variable number of repetitions of the statement (the script has to take care of renaming the copies: is there a way to make nameless declarations?), and then use the time
command with coqc
.
if by "declaration" you mean a single Coq sentence, then you can use the Time
command: https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Time
E.g., Time Definition x := 0.
Last updated: Oct 13 2024 at 01:02 UTC