[isabelle-dev] Splitting of Iptables_Semantics_Examples
makarius at sketis.net
Thu Jun 8 22:20:09 CEST 2017
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:
date: Thu Jun 08 21:01:52 2017 +0200
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.
More information about the isabelle-dev