[isabelle-dev] Splitting of Iptables_Semantics_Examples

[Makarius]

On 08/06/17 16:14, Lars Hupel wrote:
> Since AFP/b56d94d, the big session Iptables_Semantics_Examples is split
> into four smaller sessions.

For the record this is the changeset we are talking about:

changeset:   8000:b56d94d10976
user:        wenzelm
date:        Tue Jun 06 21:43:58 2017 +0200
files:       thys/Iptables_Semantics/ROOT
description:
prefer smaller sessions, notably for x86 and potentially for polyml-5.7;


That is the result of spending 1-2 days trying to figure out where the
really big parts of that session are, and what are the problems with
polyml-5.7 -- if these don't get resolved we are in a very bad
situation, sitting on a dead branch with the rather old Poly/ML 5.6.

In this process I am working together with David Matthews in the usual
way to make things eventually work again, such that Isabelle
applications can grow and prosper further.


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

The measurements of isabelle-nightly-slow are actually useable, as can
be seen here
http://isabelle.in.tum.de/devel/build_status/jenkins_isabelle-nightly-slow_64bit_8_threads/index.html

We need more such measurements for AFP, not less.


How about this?

  * Iptables_Semantics_Examples1 remains as in AFP/81a4eb593497 (in
group "slow"), it runs comfortable on x86 and takes only 35min elapsed
time with 4 cores.

  * Iptables_Semantics_Examples2 .. 4 become one big
Iptables_Semantics_Examples2 (in group "very_slow")


Thus David Matthews gets a proper test session
Iptables_Semantics_Examples1 and we routinely see its results in
http://isabelle.in.tum.de/devel/build_status


	Makarius