Re: [isabelle] AFP and Library



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.