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 <makarius at sketis.net> 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