Re: [isabelle] Algebraic_Numbers



> On 3 Jun 2016, at 7:02 AM, Makarius <makarius at sketis.net> wrote:
>
> 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.

That would be very useful!

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.