[isabelle-dev] Methods that fail with stack-overflow

[Makarius]

On Thu, 3 Jul 2014, Johannes Hölzl wrote:

> However this happened at the Scala level. Nitpick produced a huge number 
> in Suc representation, which the output panel was only possible to 
> display when the Java stack size was 16MB.

This is a "shit happens" instance on the JVM, which has a lot of technical 
weaknesses by construction, despite all the formalizations and proofs 
about its good properties.

De-facto a power user of the JVM, i.e. one of Isabelle/PIDE/Scala, needs 
to worry about certain physical parameters and re-adjust them occasionally 
depending on hardware side-conditions.  Thus it is like a Harley-Davidson.

The default JVM parameters of the Isabelle release merely try to maximize 
the chance that most users can do some useful work out-of-the box on most 
hardware and operating systems.


 	Makarius