Re: [isabelle] Algebraic_Numbers



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.

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.

Cheers,
Gerwin



> On 3 Jun 2016, at 1:24 AM, Makarius <makarius at sketis.net> wrote:
>
> On 02/06/16 16:55, Lars Hupel wrote:
>>> Thanks for this easy solution. I just pushed a corresponding change
>>> with new target: Algebraic_Number_Lib
>>
>> Because of this we now have the unfortunate situation that a significant
>> part of Algebraic_Numbers is now being built twice, without any actual
>> need to do so.
>
> Indeed. When there are bulky sessions, one should figure out how to make
> them less bulky, and not just duplicate bulkiness.
>
>
>       Makarius
>
>


________________________________

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.