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