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.


On 28 August 2017 08:15:10 CEST, Tobias Nipkow <nipkow at> wrote:
>Gerwin wrote:
>"Most AFP entries were already based on that, because weâd otherwise be
>HOL-Library about 50 times or so instead of only once per test. Itâs a
>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
>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
>> 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.