[isabelle-dev] not working

[Makarius]

On Tue, 28 Apr 2015, Larry Paulson wrote:

> Today I added some material about complex transcendental functions, and 
> then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and 
> HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the 
> latter.

I am presently not on the isabelle-dev repository, but here are some 
hints nonetheless.

> ### theory "XML_Data"
> ### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
> *** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
> *** 
> *** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")
> Unfinished session(s): HOL-Proofs-ex

The Size exception above refers to this example:

text {* Some fairly large proof: *}

ML_val {*
   val xml = export_proof @{thm Int.times_int.abs_eq};
   val thm = import_proof thy1 xml;
   @{assert} (size (YXML.string_of_body xml) > 50000000);
*}


It means that the text representation of the proof term is bigger than 
64MB, which is the limit of heap objects for Poly/ML on x86.  This may be 
seen as a reminder of invisible concrete walls that surround the whole 
game of ever growing proof libraries, walls that David Matthews has 
continuously moved further to enlarge the playground.  One day we will 
have to give up x86, though, and the entry to the game will be 16 GB 
memory.


For now it should be possible to find a different example with a smaller 
proof object instead of Int.times_int.abs_eq above, or to tune the proof 
of Int.times_int.abs_eq to reduce its recorded term size -- there might be 
something bad elsewhere that causes the sudden increase of size.


 	Makarius