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 in.tum.de> 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
>Indeed it is a trade-off and we win a little(?) by starting from a
>but we lose big time if only a single theory in Library changes. It is
>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
>> 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
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and