[isabelle-dev] HOL/Number_Theory/Primes

[Tobias Nipkow]

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.

Tobias

On 07/11/2014 15:27, Dmitriy Traytel wrote:
> This is in Isabelle2014. In 229765cc3414 I make the same measurements as Larry.
> So indeed (as the text above those lemmas suggests) there seems to be a
> regression with the simplifier setup.
>
> Dmitriy
>
> On 07.11.2014 15:10, Julian Brunner wrote:
>> The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7),
>> with the whole theory Primes loading in about 4 seconds.
>>
>> On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
>> <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>>> This theory takes quite a while to load, and I have found out why:
>>>>
>>>> text{* A bit of regression testing: *}
>>>>
>>>> lemma "prime(97::nat)" by simp
>>>> lemma "prime(997::nat)" by eval
>>>>
>>>> The proof that 97 is prime takes 35 seconds on a very fast machine. Can we
>>>> get rid of this or at least substitute a smaller number?
>>> The question is whether this has really to be performed using simp.
>>>
>>> As an alternative, a suitable code equations could be proven using the
>>> primes_upto in Eratosthenes.thy, but I did never take any measurements
>>> at which threshold the additional data structures outperform brute-force
>>> calculation.
>>>
>>>          Florian
>>>
>>> --
>>>
>>> PGP available:
>>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141107/59bc0fcc/attachment.bin>