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

Tobias Nipkow nipkow at in.tum.de
Thu Feb 21 17:02:48 CET 2013

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


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:
> 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

More information about the isabelle-dev mailing list