Hello all, 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.
Below is a minimal theory file to demonstrate the problem; I ran it with global timing turned on. theory Scratch imports "~~/src/HOL/HOL" begin 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 *) I'm using an old, slow machine, so maybe 0.253s is a bit long compared to what most people will see. On the other hand, in terms of the slowdown ratio, 0.1s or even 0.05s would be pretty bad. Here's what I learned by doing "hg bisect": 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? - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
