Re: [isabelle] Profiling tactics



On 16/03/18 11:54, Peter Lammich wrote:
> 
> 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. 

Profiling in Isabelle/ML works via the following combinators:
profile_time, profile_time_thread, profile_allocations -- these are
based on mechanisms provided by the Poly/ML runtime system.

The result is somewhat unstructured, though: it measures everything that
happens globally in the running ML program. For profile_time_thread that
is restricted to the current thread -- it may be used only on a single
thread at a time.


Profiling tactics is more challenging, due to lazy evaluation and
multiple results (for potential backtracking). I usually do this by
pushing the profiling to the bottom of it (e.g. the Simplifier
invocation behind simp_tac) or to the top (e.g. the outermost apply
command: it has only one result).

Here is also a tactical (from src/HOL/Tools/Nitpick/nitpick_util.ML)
that make a tactic behave like a strict deterministic function and
applies a timeout to it:

fun DETERM_TIMEOUT delay tac st =
  Seq.of_list (the_list (Timeout.apply delay (fn () => SINGLE tac st) ()))

The same approach should work e.g. with profile_time_thread instead of
Timeout.apply, but the potential for backtracking will get lost.


	Makarius





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