Re: [isabelle] AFP and Library



On 28/08/17 08:15, Tobias Nipkow 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."

This is indeed the traditional explanation for providing various
"library" images in Isabelle and using them in the applications, e.g. in
AFP. In recent years we have seen a trend of increasing that quite
substantially.

In particular, Isabelle2017 will have the following important starting
points for applications:

  HOL
  HOL-Library
  HOL-Computational-Algebra
  HOL-Analysis | HOL-Algebra | HOL-Number_Theory | HOL-Nonstandard-Analysis

After changing any of them, there will be substantial follow-up build
times of other sessions depending on them. This is a natural consequence
of providing good library sessions and getting lots of applications on top.


There is a second aspect for the HOL-Library image only: it is somehow
the canonical supplement to the main HOL image.

Thus there are occasional tendencies in the applications to provide a
session "Foo" and also "Foo-Library" that "merges" the HOL-Library
aspect later on, even after building a whole stack of sessions. This
complicates session specifications and causes further multiplication of
build times. Since we cannot really merge session images, the main
approach to avoid the problem is to put HOL-Library at the very start of
the session dependencies and to remove the Foo-Library variant eventually.


> 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.

This sounds more like the file-based build model of Coq, but without
actual "object files" to store intermediate states.

It is a theoretical question if we can move over there, practically we
can't change the fundamental approache on the spot and expect that
things still work afterwards.

(I have occasionally discussed the inherent differences of the build
model with the Coq guys, and am still convinced that our tradition of
doing it scales better. Empirical proof: size and complexity of AFP today.)


I do agree that in the past 1-2 years there is an increasing pain to be
felt in maintaining Isabelle + AFP, up to the point that less
maintenance and fewer important reforms happen. In the past 3 years, the
size of Isabelle + AFP material has doubled, while build and test
infrastructure had stagnated since 2012. Only recently this has improved
again (but I don't mean the Jenkins setup, which I simply ignore).

What would greatly help is to have proper time measurement for nightly
builds of AFP within the regular Isabelle cronjob, with its persistent
database support in the background (see also
http://isabelle.in.tum.de/devel/build_status). The software is all there
in Isabelle/Scala; lacking is only some half-decent test hardware (e.g.
a cloud node with 8 cores + 64 GB should be sufficient).

At some point, "isabelle build" could use the persistent timing
information from the database to make better scheduling of big builds,
including adhoc changes to the actual session graph (e.g. changing
parent sessions vs. session imports).


	Makarius




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