Re: [isabelle] Exception size raised



Dear Makarius,

Thank you for your reply.
The reason I'm using the 2015, is because I'm using Haskabelle
and after having troubles with the 2016 (I wasn't able to do anything with
it),
I downgraded to 2015, and it works out of the box.
However, I'm following your tip, and I'm using the 2016-1 version, and it
now
is running with ML System 64. Let's hope it works now. Although, it still
takes several minutes to print any answer, with a subset of my stuff.

Many thanks,

On 23 December 2016 at 11:18, Makarius <makarius at sketis.net> wrote:

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


-- 
Artur Oliveira Gomes
PhD Student - SCSS - Trinity College Dublin
Professor - Sistemas de InformaÃÃo - UFMS



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