Hi, yes you are right. I closed all applications and reset the dropdown to HOL instead of pure. With everything closed the system was using 740 mb on 3 cores. Then upon building when "Hol theory Code_Evaluation" is reached, usage goes up to 3.7GB and then later goes down to 3.6GB. Then at "Hol: theory Complex_main" it goes back up to 3.7GB (by which time swap usage is 86%). Then after a long time memory usage goes down and this time the build is successful.
Thanks On Thu, Feb 4, 2016 at 12:08 PM, Makarius <[email protected]> wrote: > On Thu, 4 Feb 2016, Artella Coding wrote: > > I have 4GB allocated to my virtual machine (the laptop actually has 8GB) >> but selecting the "Pure" in the theories dropdown stops the HOL theories >> being build, which was what was consuming so much memory. Thanks >> > > Isabelle/HOL is big, but it should definitely build on 4GB in 64bit mode. > > Can you provide more VM parameters? Number of cores? Linux version? > > > Isabelle/HOL may be also seen as a benchmark for the PIDE. Using Pure as > a basis and loading $ISABELLE_HOME/src/HOL/Main.thy (with all its > requirements as proposed by the system), it loads tons of ML modules plus > surrounding theories. > > It is then possible to go to ML_file commands (e.g. via jEdit hypersearch > over all buffers), and follow the hyperlinks to the corresponding source > files. > > This requires definitely 8GB. > > Note that a shade of pink means the system is still working towards that > point of text. The Theories panel helps to keep an overview. > > > Makarius >
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
