Re: [isabelle] problem with the last development snapshot



On Thu, 20 Sep 2007, Temesghen Kahsai wrote:

> Started at Thu Sep 20 17:44:31 BST 2007 (polyml-4.1.4_ppc-darwin on
> cslttk.swan.ac.uk)
> Building Pure ...
> Finished Pure (0:00:55 elapsed time, 0:00:34 cpu time)
> Building HOL ...
> Run out of store - interrupting console processes
> HOL FAILED
> (see also
> /usr/local/share/Isabelle_20-Sep-2007/heaps/polyml-4.1.4_ppc-darwin/log/HOL)

It seems that Isabelle/HOL has recently grown too fat for Poly/ML 4.x on 
ppc, which uses slightly more memory than x86 so we did not notice yet.

Luckily Poly/ML 5.0 is reasonably stable for production use right now, 
although it can also run into situations where the stack cannot be 
increased despite plenty of free memory being available.

The still emerging Poly/ML 5.1 (available via CVS) won't have any of these 
problems and you can already play around with multicore machines right 
now.

See http://www.polyml.org/download.html for further details.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.