[isabelle-dev] exception Size raised (line 173 of "./basis/LibrarySupport.sml")
makarius at sketis.net
Thu Feb 21 15:56:13 CET 2013
On Thu, 21 Feb 2013, Tobias Nipkow wrote:
> Load attached theory in HOL/IMP. Go to line
> done (* exception *)
> and you'll see the subject line.
> I am on parent: 51188:9b5bf1a9a710 tip
The exception means that some string value has exceeded String.maxSize,
which is approx. 64 MB on the 32bit platform that we are using by default
Enabling exception trace like this
ML_command "Toplevel.debug := true"
produces the following:
Florian should know what to do here.
There are often easy ways to avoid huge monolithic strings, e.g. via type
Buffer.T instead of string. If it turns out complicated, one needs to
More information about the isabelle-dev