[isabelle] Profiling tactics



Hi,

are there any tools to profile tactics in Isabelle?

I basically have a tactic of the form

  REPEAT ( tac1 ORELSE ... ORELSE tacN )

I want to figure out how long each of the tactics runs, to identify
hot-spots for optimization. 

I may need to do this in a nested way, e.g.

  tac1 = tac12 THEN simp_tac ...

and I want to know how much time is spent on the simplification.


Is there any (how basic so-ever) support for such profiling? I'm only
aware of the timing panel, which is very cumbersome to use for this
case, as it displays the timings of all commands, and cannot be focused
on the command(s) I'm interested in. 

For first, It would be enough if "apply" and "back" could output the
required time, depending on a configuration flag (this option used to
be in old Isabelles, but has apparently be removed in favour of the
timing panel?) Then I could unfold a particular run of my tactic into a
sequence of apply and back, and see the relevant timings.

Of course I would be happy to hear of any more advanced profiling
techniques available for Isabelle.


--
  Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.