Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples
> The idea is to have a somewhat manageable chop from > Iptables_Semantics_Examples within the range of a build with standard > parameters (which means x86), merely guarded by "slow" group tag. > > Thus it is visible in tests like "isabelle build -d '$AFP' -a -X > very_slow" that I am doing manually all the time, e.g. when there is a > change in the Poly/ML repository. > > Since we did not have that for the huge Iptables_Semantics_Examples last > year, we ran blindly into the unpleasant surprise of a Poly/ML 5.7 > version that no longer worked for us. Ironically, this has now exhibited a problem in 5.6: poly: scanaddrs.cpp:218: void ScanAddress::ScanAddressesInRegion(PolyWord*, PolyWord*): Assertion `obj->ContainsNormalLengthWord()' failed. I have seen that once or twice before. I thought it was spurious, but perhaps it should be investigated more. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples
On 08/06/17 17:09, Lars Hupel wrote: >> 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. > > That makes sense. OK, I have changed it now as follows: changeset: 8013:8262cf67ba80 user:wenzelm date:Thu Jun 08 21:01:52 2017 +0200 files: thys/Iptables_Semantics/ROOT description: clarified example sessions: Iptables_Semantics_Examples runs on x86 in approx. 30min elapsed time (4 cores), but Iptables_Semantics_Examples_Big requires x86_64 and several hours; > So, is it your plan to re-merge these sessions if > these problems get resolved? The idea is to have a somewhat manageable chop from Iptables_Semantics_Examples within the range of a build with standard parameters (which means x86), merely guarded by "slow" group tag. Thus it is visible in tests like "isabelle build -d '$AFP' -a -X very_slow" that I am doing manually all the time, e.g. when there is a change in the Poly/ML repository. Since we did not have that for the huge Iptables_Semantics_Examples last year, we ran blindly into the unpleasant surprise of a Poly/ML 5.7 version that no longer worked for us. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples
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
