[isabelle-dev] exception Size raised (line 173 of "./basis/LibrarySupport.sml")
makarius at sketis.net
Thu Feb 21 16:51:48 CET 2013
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
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.
More information about the isabelle-dev