[isabelle-dev] polyml-5.7-20170217

[Makarius Wenzel]

On 17/02/2017 22:41, Makarius wrote:
> With Isabelle/42b92fa72a51 we are on a pre-release version of Poly/ML
> 5.7. David Matthews is about to converge to a release.
>
> There are various changes in the runtime system, and a few ones in the
> compiler (more PIDE markup). For example, local identifier scopes are
> visualized in the Isabelle/ML IDE as for the logical term language.

I have seen problems to build the HOL image on my new macOS Sierra test 
machine (which is a bit underpowered). It helps to provide more initial 
heap space, e.g. like this in etc/settings:

ML_OPTIONS="-H 1000"

Alternatively, it also helps to build with -o threads=1.


Maybe this is a symptom of Mac OS X memory management problems that 
we've occasionally seen in recent years.


	Makarius