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

[Makarius]

On Thu, 21 Feb 2013, Makarius wrote:

> This is how to configure x86_64 in $ISABELLE_HOME_USER/etc/settings:
>
>  ML_PLATFORM="$ISABELLE_PLATFORM64"
>  ML_HOME="$ML_HOME/../$ML_PLATFORM"
>

Actually doing this reveals further resource limitations.  First of all, 
Oracle needs to be instructed to provide a bit more heap space like this:

JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"

See also ~~/src/Tools/jEdit/etc/settings for some more examples.


Then the goal can be printed and digested by the front-end, but it is all 
very huge and takes minutes to get through.


Here is some ML snipped to get an idea about size of output:

ML_val {*
   fun pr_size st =
     size (Pretty.string_of (Pretty.chunks (Proof.pretty_state 1 (Toplevel.proof_of st))));

   pr_size @{Isar.state};  (* with PIDE markup *)
   (* 139371907 *)

   Print_Mode.setmp [] pr_size @{Isar.state};  (* raw output *)
   (* 15882084 *)
*}

130 MB is a bit much for the whole syntax stack and editor front-end, but 
it is only factor 2 beyond the 64 MB string limit in 32bit mode.

15 MB for the raw text is also quite something.  We also see that PIDE 
markup is only a factor 10 larger, even though it marks all formal 
entities and type information for atomic subterms.  (The type information 
is approx. a factor of 2, but I did not measure this here.)


We are presently in this bounded 32bit address space by default, which is 
2GB .. 3.5 GB depending on the platform. I find its early failure 
behaviour more convenient, than denial of service of the overall system. 
For example, certain situations of non-termination produce a Interrupt 
exception due to stack overflow, instead of filling up VM space 
indefinitely.


 	Makarius