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 < [email protected]> 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 <[email protected]> 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 >> [email protected] >> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> > >
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
