Re: [isabelle] AFP and Library



Just as a side note for your consideration: Jenkins builds the AFP incrementally, i.e., only changed sessions. A change in HOL-Library will entail a lot of sessions being rebuilt, even if just a single theory has changed.

Maybe we should look into which library theories change the most or split library into multiple sessions.

Cheers
Lars

On 28 August 2017 08:15:10 CEST, Tobias Nipkow <nipkow at in.tum.de> wrote:
>Gerwin wrote:
>
>"Most AFP entries were already based on that, because weâd otherwise be
>building 
>HOL-Library about 50 times or so instead of only once per test. Itâs a
>trade-off."
>
>Well, we would only be building a few popular entries in Library
>multiple times. 
>Indeed it is a trade-off and we win a little(?) by starting from a
>Library image 
>but we lose big time if only a single theory in Library changes. It is
>a bit 
>like amortized complexity: on average, you win, but in real time you
>may have to 
>wait much longer. Since Library changes frequently, I do wonder about
>this 
>trade-off.
>
>Tobias
>
>On 27/08/2017 13:35, Tobias Nipkow wrote:
>> Hi Makarius,
>> 
>> You have concerted many if not all AFP sessions that use theories
>from Library 
>> such that they are now based on the Library image. This means that
>every time a 
>> Library theory changes, sonething like half the AFP needs to be
>rebuilt even 
>> though only a few of the AFP sessions may import the modified Library
>theory. 
>> This happens fairly frequently and I wonder what your rational for
>the change was.
>> 
>> Tobias
>> 



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