coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Profiling Coq Code

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Profiling Coq Code
Date: Wed, 2 Jan 2013 17:15:05 -0500

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

[Coq-Club] Profiling Coq Code, Jason Gross, 01/02/2013
- Re: [Coq-Club] Profiling Coq Code, Thomas Braibant, 01/03/2013
- Re: [Coq-Club] Profiling Coq Code, Gregory Malecha, 01/03/2013