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

[Tobias Nipkow]

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")?

Tobias

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