*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:32:28 +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: > For comparison, weâre doing this already: since we canât merge multiple parent sessions, all entries that re-use more than one other entry will currently definitely rebuild all of at least one parent anyway. Given that, and the effort Iâm spending periodically to make sure the AFP does not rebuild HOL-Library 100 times each day, I donât think the light part of one entry being rebuilt is a problem. BTW, for years I am trying to get to a situation where sessions and heap images are independent (also for document preparation). That would allow to run many AFP sessions within the same Poly/ML process, providing a chance that the big number of small sessions uses much less resources. Makarius

**Follow-Ups**:**Re: [isabelle] Algebraic_Numbers***From:*Gerwin Klein

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