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