*To*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Subject*: Re: [isabelle] Algebraic_Numbers*From*: Makarius <makarius at sketis.net>*Date*: Thu, 2 Jun 2016 23:23:04 +0200*Cc*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, Lars Hupel <hupel at in.tum.de>, Manuel Eberl <eberlm at in.tum.de>, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <E3369AA1-D02B-4D31-94A6-A40F3A212315@nicta.com.au>*References*: <34d483c8-0558-11f6-a1f3-d5932e44cfb0@in.tum.de> <574FE349.9040606@informatik.tu-muenchen.de> <E1491251-20E2-4993-A058-5167D9C88F77@uibk.ac.at> <251ba710-5d97-3eee-7a24-ca07fbbc7f3b@in.tum.de> <696C6BAF-9C2F-40BE-AEEE-0F0B336FF7A2@nicta.com.au> <1667CB23-B68C-42A9-BF7D-2FACD8C6CE24@uibk.ac.at> <bc6ee781-85b8-2f94-13d8-5bca02064470@in.tum.de> <57504FA9.3010008@sketis.net> <E3369AA1-D02B-4D31-94A6-A40F3A212315@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 02/06/16 22:37, Gerwin Klein wrote: > I thought the point was that the part that is duplicated is *not* bulky. If it is, we should think more, but I donât have any better solutions ready. I think the worries of Lars Hupel are based on the rather weak Isabelle/Jenkins testing hardware. My own worries are based on general observations that Algebraic_Numbers could be close to the infamous "invisible concrete wall" (without detailed measurements yet). Here are some numbers on the fastest test machine that I have access to (i.e. my own workstation): Isabelle/bcf4828bb125 + AFP/83c0fef83e3f x86-linux, 6 threads Finished Algebraic_Number_Lib (0:00:48 elapsed time, 0:04:12 cpu time, factor 5.22) ## without heap image Finished Algebraic_Numbers (0:04:48 elapsed time, 0:22:56 cpu time, factor 4.78) ## based on Pre_Algebraic_Numbers Now the same, but Algebraic_Numbers is based on Algebraic_Number_Lib, i.e. the first session builds a heap and the second only runs the bulky tests: Finished Algebraic_Number_Lib (0:01:17 elapsed time, 0:05:28 cpu time, factor 4.23) Finished Algebraic_Numbers (0:03:54 elapsed time, 0:17:54 cpu time, factor 4.57) This makes some difference in overall CPU time usage. It is reminiscent of ancient times, when Jinja (not JinjaThreads) had to be split into two sessions: the full compactification of the first heap makes the second one more comfortable. Although the effect today is not that important, due to online heap sharing. There are already AFP entries with more than one session, and also add-on documents. Maybe that is already sufficient to publish the tests separately, or maybe not. Lars Hupel might be able to say that. Stepping back further, the question is why Algebraic_Number_Tests requires so much persistent heap memory that sessions built on it might get into problems. Maybe there is a deeper resource problem behind it. Makarius

**Follow-Ups**:**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

**References**:**[isabelle] Algebraic_Numbers***From:*Manuel Eberl

**Re: [isabelle] Algebraic_Numbers***From:*Florian Haftmann

**Re: [isabelle] Algebraic_Numbers***From:*Thiemann, Rene

**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

**Re: [isabelle] Algebraic_Numbers***From:*Lars Hupel

**Re: [isabelle] Algebraic_Numbers***From:*Makarius

**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] Algebraic_Numbers
- Next by Date: Re: [isabelle] Algebraic_Numbers
- Previous by Thread: Re: [isabelle] Algebraic_Numbers
- Next by Thread: Re: [isabelle] Algebraic_Numbers
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list