Stream: Coq users

Topic: timing a declaration?


view this post on Zulip Scott Morrison (Sep 21 2023 at 00:29):

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.

view this post on Zulip Karl Palmskog (Sep 21 2023 at 05:16):

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: Jun 23 2024 at 05:02 UTC