*To*: Gerwin Klein <Gerwin.Klein at nicta.com.au>, Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Algebraic_Numbers*From*: Makarius <makarius at sketis.net>*Date*: Sat, 4 Jun 2016 14:12:31 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <62201F35-4456-4882-A419-19ACC4E8DABD@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> <5750A3B8.4070208@sketis.net> <3f5f60a7-1f09-b92c-926b-37cfc97dbde4@in.tum.de> <62201F35-4456-4882-A419-19ACC4E8DABD@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

On 04/06/16 02:34, Gerwin Klein 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. > > Does sound worth investigating, I have no direct ideas either. > > Maybe it is indeed time to officially enable multiple sessions for AFP entries. That will take some infrastructure work, but it would give us more flexibility in treating things like this, for instance with the technique Makarius mentioned, which we used for Jinja years back. The split into two sessions had mainly the effect to enforce a full heap compaction (and reload). In contempory Poly/ML this can be done at runtime, e.g. by putting this into a suitable place (e.g. Algebraic_Number_Tests.thy): ML_command %invisible \<open>ML_Heap.share_common_data ()\<close> Here are some measurements for Isabelle/d8884c111bca + AFP/44c49a721891 on x86-linux with 6 threads. (0) standard setup: Finished Algebraic_Numbers (0:04:21 elapsed time, 0:20:03 cpu time, factor 4.60) (1) ML_command share_common_data: Finished Algebraic_Numbers (0:05:23 elapsed time, 0:23:52 cpu time, factor 4.43) (2) Algebraic_Numbers based on Algebraic_Number_Lib: Finished Algebraic_Number_Lib (0:01:18 elapsed time, 0:05:31 cpu time, factor 4.21) Finished Algebraic_Numbers (0:04:07 elapsed time, 0:17:55 cpu time, factor 4.34) The times for (1) are approximately equal to the sums of times for (2). Maybe Lars can try share_common_data on the AFP test hardware to see if it still happens to work on 32bit architecture. 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

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

- Previous by Date: Re: [isabelle] Algebraic_Numbers
- Next by Date: [isabelle] Set Comprehention {5n. nâN} without existence-quantor?
- 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