[isabelle-dev] Splitting of Iptables_Semantics_Examples

Lars Hupel hupel at in.tum.de
Thu Jun 8 16:14:29 CEST 2017


Since AFP/b56d94d, the big session Iptables_Semantics_Examples is split
into four smaller sessions.

This poses a problem for the nightly job, which is running with -j1 and
threads=8. The parallelism in the four smaller sessions is much less
than the parallelism (factor 3) in the previous big session (factor 6).
This can be witnessed by the big jump in build time from build #441 to #442:


<https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/buildTimeTrend>

In fact, it takes longer than the hard-coded timeout of 20 hours for the
full job. Starting tomorrow, the build timeout will be 23.5 hours. (I'm
not sure whether or not that increase is sufficient.)

Still, this is somewhat unsatisfactory, because it means that the
maintenance window shrinks to some time between 2am and 3am CET.

There are two ways to avoid these excessive build times:

1) Backing out AFP/b56d94d.
2) Changing to -j2 with threads=4. This has the downside that there will
be a jump in measurements of JinjaThreads etc. Then again, I don't know
if anyone even looks at the statistics for isabelle-nightly-slow.

Cheers
Lars


More information about the isabelle-dev mailing list