Email Gateway (Aug 22 2022 at 16:57): Email Gateway (Aug 22 2022 at 16:57):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 17:00):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 17:00):From: Makarius <makarius@sketis.net>
The timing tooltip for 'back' was last working before this changeset:
changeset: 51595:8e9746e584c9
user: wenzelm
date: Tue Apr 02 11:41:50 2013 +0200
files: src/Pure/Isar/toplevel.ML src/Pure/PIDE/command.ML
description:
more centralized command timing;
clarified old-style timing message;
The change is not directly relevant, though. The deeper reason is an
accidental change of order of markup for a command with arguments
('apply') and one that consists of a single keyword ('back'). Apparently
nobody noticed it, because 'back' is used very rarely these days.
I have now refined that here:
changeset: 67933:604da273e18d
tag: tip
user: wenzelm
date: Fri Mar 23 17:09:36 2018 +0100
files: src/Pure/PIDE/rendering.scala
description:
more robust timing info: do not rely on order of markup;
Included is a small example. I have used the APPEND tactical here,
because it preserves all possibilities for backtracking. The ORELSE
tactical (which corresponds to "|" in Isar) commits on the first success
and ignores the remaining possibilities.
Makarius
Scratch.thy
Last updated: Apr 23 2024 at 20:15 UTC