<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">The culprit seems to be dvd_imp_mod_0
introduced as a simp rule in 773b378d9313.<br>
<br>
The following takes again only 2 seconds.<br>
<br>
declare dvd_imp_mod_0[simp del]<br>
lemma "prime(97::nat)" by simp<br>
<br>
Dmitriy<br>
<br>
On 07.11.2014 15:31, Tobias Nipkow wrote:<br>
</div>
<blockquote cite="mid:545CD7BC.3090507@in.tum.de" type="cite">Very
nice observations, thank you. I was obviously too hasty to remove
the test which exposed this time leak. Once this issue has been
fixed, I will put the "long" test back in, with a better comment.
<br>
<br>
Tobias
<br>
<br>
On 07/11/2014 15:27, Dmitriy Traytel wrote:
<br>
<blockquote type="cite">This is in Isabelle2014. In 229765cc3414 I
make the same measurements as Larry.
<br>
So indeed (as the text above those lemmas suggests) there seems
to be a
<br>
regression with the simplifier setup.
<br>
<br>
Dmitriy
<br>
<br>
On 07.11.2014 15:10, Julian Brunner wrote:
<br>
<blockquote type="cite">The proof that 97 is prime only takes
1.3s on my machine (2.7 GHz i7),
<br>
with the whole theory Primes loading in about 4 seconds.
<br>
<br>
On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
<br>
<a class="moz-txt-link-rfc2396E" href="mailto:florian.haftmann@informatik.tu-muenchen.de"><florian.haftmann@informatik.tu-muenchen.de></a> wrote:
<br>
<blockquote type="cite">
<blockquote type="cite">This theory takes quite a while to
load, and I have found out why:
<br>
<br>
text{* A bit of regression testing: *}
<br>
<br>
lemma "prime(97::nat)" by simp
<br>
lemma "prime(997::nat)" by eval
<br>
<br>
The proof that 97 is prime takes 35 seconds on a very fast
machine. Can we
<br>
get rid of this or at least substitute a smaller number?
<br>
</blockquote>
The question is whether this has really to be performed
using simp.
<br>
<br>
As an alternative, a suitable code equations could be proven
using the
<br>
primes_upto in Eratosthenes.thy, but I did never take any
measurements
<br>
at which threshold the additional data structures outperform
brute-force
<br>
calculation.
<br>
<br>
Florian
<br>
<br>
--
<br>
<br>
PGP available:
<br>
<a class="moz-txt-link-freetext" href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de">http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a>
<br>
<br>
<br>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
<br>
</blockquote>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
</blockquote>
<br>
_______________________________________________
<br>
isabelle-dev mailing list
<br>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<br>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
<br>
</blockquote>
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>