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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to