Re: [isabelle] Profiling tactics

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

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
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
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.

theory Scratch
  imports Pure

ML \<open>
fun sleep_tac t st =
  if Method.detect_closure_state st then Seq.empty
  else (OS.Process.sleep t; Seq.single st);

lemma "PROP A"
  apply (tactic \<open>sleep_tac (seconds 0.5) APPEND sleep_tac (seconds 1.0)\<close>)


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