Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples

[Lars Hupel]

> 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

[Makarius]

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

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

[isabelle-dev] Splitting of Iptables_Semantics_Examples

[Lars Hupel]

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:




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