[isabelle-dev] Methods that fail with stack-overflow
makarius at sketis.net
Thu Jul 3 18:45:56 CEST 2014
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.
More information about the isabelle-dev