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

[Tobias Nipkow]

Now that I know that this is a resource limitation and not an error, I'm happy
again.

Thanks
Tobias

Am 21/02/2013 16:51, schrieb 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