[isabelle-dev] Failures of Iptables_Semantics

[Makarius]

On 31/08/2024 13:51, Lawrence Paulson wrote:
> Why do we keep getting this? Iptables_Semantics runs fine on my machine.
 >
> Finished Iptables_Semantics (0:00:42 elapsed time, 0:03:29 cpu time, factor 4.94)
> 0:01:04 elapsed time, 0:03:29 cpu time, factor 3.25

I've spent more time with Iptables_Semantics_Examples and 
Iptables_Semantics_Examples_Big, and now understand the situation much better.

Here is a summary:

   * The Iptables_Semantics material has always been wasteful about ML 
resources and occasionally caused problems after minor changes here and there. 
Some years ago it routinely required ML_system_64 with 30g ML heap, but 
recently it happened to fit into the default 64_32 memory model (which is good).

   * My change in Isabelle/70076ba563d2 has introduced a lot of extra markup: 
for every comma in enumerations of sets, tuples, lists. Moreover, I 
accidentally destroyed the printing of char list as string literal.

   * Consequently, the output of 'value' commands in the Iptables_Semantics 
sessions has grown significantly, e.g. 500 MB instead of 5 MB in line 177 of 
Iptables_Semantics/Examples/IPPartEval/IP_Address_Space_Examples_All_Small.thy 
--- less drastic in other situations.

   * With Isabelle/5e38e8b34eb3 we should be back to normal concerning string 
literals (which don't have extra markup).


	Makarius