[isabelle-dev] exception Size raised (line 173 of "./basis/LibrarySupport.sml")

[Makarius]

On Thu, 21 Feb 2013, Tobias Nipkow wrote:

> It is a fairly huge goal state that is supposed to get printed there. 
> With all the annotations, it may exceed the limit. But why is code 
> generation involved at that point ("done")?

The exception trace has no context, so I just looked in the wrong spot -- 
one of the later 'value' commands in the text.  So Florian can ignore 
this thread.


Trying again in TTY mode, there is indeed a huge error message produced 
here.  It crashes when run with full annotations in Isabelle/jEdit.

The computer is a finite automaton, it will always crash at some point. 
You can either use x86_64 for the proof development, or try to avoid such 
massive goals in the first place.

This is how to configure x86_64 in $ISABELLE_HOME_USER/etc/settings:

   ML_PLATFORM="$ISABELLE_PLATFORM64"
   ML_HOME="$ML_HOME/../$ML_PLATFORM"

Note that everything that ends up in the Isabelle or AFP repository needs 
to run in batch mode for x86 in 32bit mode.  This is faster on Linux and 
Mac OS X, and on Windows/Cygwin x86_64 is unavailable.


 	Makarius