[isabelle-dev] Splitting of Iptables_Semantics_Examples

Lars Hupel hupel at in.tum.de
Fri Jun 9 16:44:56 CEST 2017

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


More information about the isabelle-dev mailing list