Re: [isabelle] Exception size raised



On 22/12/16 21:24, Artur Gomes wrote:
> 
> I'm using Isabelle2015 on OS X (El Captain),
> and after a few minutes waiting for Isabelle to
> load a function definition of mine, I got the following
> message:
> "exception Size raised (line 139 of "./basis/LibrarySupport.sml")"
> Is there any way to identify what's going on? Or maybe
> a way to allocate more resources to Isabelle?

Step 0: try the current official release Isabelle2016-1 (December 2016).
Historic Isabelle versions should not be used anymore, unless there are
special reasons for that.

Step 1: You can try the 64bit version of Isabelle/ML, by enabling the
option ML_system_64, e.g. in Isabelle/jEdit "Plugins / Plugin Options /
Isabelle / General / ML System 64". Then restart / rebuild the
application. In 64bit mode the only limit are available system
resources, so instead of a Size exception (e.g. for strings and other
blobs > 64 MB) there might be a total existence failure of the ML
process without exception :-) :-(


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.