The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

It happens that I developed a plugin that does that. You can find it here.
https://github.com/braibant/Timing-plugin

It provides low level counters that one can start and stop, typically
used as wrappers around a given tactic (e.g., Ltac foo a b c :=
start_timer "foo"; myTac a b c; stop_timer "foo".) and some vernacular
commands to display the timings recorded so far.

Thomas
(NB: I have not bumped the version it works with to 8.4pl1, but it
should work fine with that one.)

On Wed, Jan 2, 2013 at 11:15 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Hi,
> Is there a way to profile Ltac code, i.e., to get a list of how much time is
> spent in each Ltac fragment (such as [apply MyTheorem], [apply f_equal],
> [myTac a b c])?
>
> Thanks.
>
> -Jason