The build process which ends up consuming too much memory says :
******* Isabelle build (polyml-5.6_x86_64-linux / jdk-8u72_x86_64_linux)
Build started for Isabelle/HOL... Building HOL... HOL:theory ... ... *******
Is there any way of configuring the maximum amount of memory this build process uses? Thanks
On Wed, Feb 3, 2016 at 9:15 AM, Artella Coding < artella.coding at googlemail.com> wrote:
Hi, I thought I would give this a try (I know nothing about Isabelle or HOL). So I downloaded the executable at http://isabelle.in.tum.de/website-Isabelle2016-RC3/ and then ran ./Isabelle2016-RC3
At first it started building loads of files but I ran out of memory so had to stop that building. Then I noticed a src/Tools/SML/Examples.thy in the "Examples" dropdown in the "Documentation" tab on the right. So clicking this opens the file, but I am not sure how to compile and run this file. I looked at some online videos but they didnt really help. So how do I compile and run the src/Tools/SML/Examples.thy file?
Thanks
On Mon, Feb 1, 2016 at 7:07 PM, Makarius <makarius at sketis.net> wrote:
Dear users of the best unknown programming language in the world.
Isabelle/ML is based on Poly/ML and thus benefits from the source-level debugger of that implementation of Standard ML. The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context.
More explanations with a screenshot on http://sketis.net/2016/ml-debugging-within-the-prover-ide
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml