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