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
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
