*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Algebraic_Numbers*From*: Makarius <makarius at sketis.net>*Date*: Fri, 3 Jun 2016 23:33:44 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <3f5f60a7-1f09-b92c-926b-37cfc97dbde4@in.tum.de>*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> <5750A3B8.4070208@sketis.net> <3f5f60a7-1f09-b92c-926b-37cfc97dbde4@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 03/06/16 23:17, Lars Hupel wrote: > >> 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. > > That is an excellent question. I still can't quite put my finger on it > as to why that single theory forces us to run AFP tests in bulky 64 bit > mode. I did not know that the situation is that bad. An important point if AFP tests is to see if everything still works nicely in the small x86 heap model. That is one aspect of the "invisible concrete wall". Makarius

**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

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

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

- 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