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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev