Email Gateway (Aug 22 2022 at 14:42): Email Gateway (Aug 22 2022 at 14:42):From: Artur Gomes <gomesa@tcd.ie>
Hi there,
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?
Regards,
Email Gateway (Aug 22 2022 at 14:43):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 22 2022 at 14:43):From: Artur Gomes <gomesa@tcd.ie>
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,
Email Gateway (Aug 22 2022 at 14:43):From: Makarius <makarius@sketis.net>
This sounds like there is something odd with your application. How big
are your function definitions? What form do they have?
If something takes unreasonably long, or requires unreasonable amounts
of resources, it needs to be formulated differently.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC