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:
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:
date: Fri Mar 23 17:09:36 2018 +0100
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.
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