[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