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

[Makarius]

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 
everywhere.

Enabling exception trace like this

   ML_command "Toplevel.debug := true"

produces the following:

Code_Target.prepare_serializer(17)
Code_Target.mount_serializer(9)
Code_Runtime.obtain_evaluator(6)
Code_Runtime.evaluation(5)
Code_Preproc.dynamic_value(4)
Code_Evaluation.gen_dynamic_value(1)(1)(1)
Value.value_cmd(4)
Toplevel.apply_tr(3)(1)


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 
think again.


 	Makarius