On Thu, 11 Aug 2011, Brian Huffman wrote:
Recently I've been hacking on a bunch of proof scripts using the
development version of Isabelle, and I noticed that when processing
proof scripts, I often get a noticeable pause at uses of "simp_all". The
same pause does not occur with Isabelle2011.
lemma shows "True" and "True"
by (simp, simp)
(* 0.001s elapsed time, 0.000s cpu time, 0.000s GC time *)
lemma shows "True" and "True"
by simp_all
(* 0.253s elapsed time, 0.004s cpu time, 0.000s GC time *)
This is indeed a bit slow, although it is not CPU time, only some latency
of the tty loop (which is inherently synchronous and thus slow).
http://isabelle.in.tum.de/repos/isabelle/rev/aaaa13e297dc improves startup
time of the worker thread farm significantly, and I've got real times in
the range of 0.003s -- 0.005s on my "old" machine from 2 years ago with
Proof General.
Really old machines with only 1 core should not experience any slowdown
from the parallel combinator, because multithreading is not enabled.
The first bad revision is:
changeset: 42372:6cca8d2a79ad
user: wenzelm
date: Sat Apr 16 23:41:25 2011 +0200
summary: PARALLEL_GOALS for method "simp_all";
http://isabelle.in.tum.de/repos/isabelle/rev/6cca8d2a79ad
Was this change supposed to *improve* performance? Was the performance
impact tested? Maybe the performance penalty only appears when
interactively stepping through proofs, and not in batch mode?
Yes, it improves some sessions like HOL-Hoare_Parallel, probably also some
larger AFP ones, but we still don't have any old-style isatest statistics.
The worst-case overhead for batch mode should be neglible -- same for
Isabelle/jEdit which is closer to batch mode than PG tty mode.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
