[isabelle-dev] Splitting of Iptables_Semantics_Examples

[Lars Hupel]

> 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. So, is it your plan to re-merge these sessions if
these problems get resolved?

Right now we have the unfortunate restriction that there are two
different "layers" of parallelism (parallel sessions vs. threads in a
session), and for sessions with many independent theories it is
preferable to err on the side of threads in a session. I'd assume that
to unifying this is a large-scale project.

> 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")

That would be fine with me. The speedup factor is <4 but since it's less
than an hour elapsed time on the LRZ machine I think we can take that hit.

Cheers
Lars