Re: [isabelle] AFP and Library



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.

Tobias

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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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