On 28/08/2017 09:07, Lars Hupel wrote:
Maybe we should look into which library theories change the most or split library into multiple sessions.
Thank you for this constructive suggestion. What would happen if there was an AFP_Library with only those Library theories that are needed at least twice in the AFP? I analyzed the sources. Only half the theories in Library are used at least twice in the AFP. Then I analyzed the last 123 builds on Jenkins: 13 of them did not involve any theory in AFP_Library and the AFP build would have completed much more quickly (often in a few minutes rater than 1 hour). There is an argument here for a dedicated AFP_Library.
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
Description: S/MIME Cryptographic Signature