Re: [isabelle] Building with SML/NJ

On Wednesday 31 December 2008 01:18:24 Makarius wrote:
> Note that everything we provide by default is based on Poly/ML, see also
> if you really want to compile from scratch.  I am
> including the README of our distribution, which tells how binaries have
> been produced.  You can also download our Poly/ML tar.gz files and then
> build only the logic images.
> SML/NJ used to be an alternative many years ago, but the relative
> performance compared to Poly/ML has changed so much to render it
> impractical -- for two reasons: (1) big heap space makes NJ inherently
> slow due to its stackless execution model, (2) NJ is single-threaded, but
> starting with Poly/ML 5.1 we have native Posix threads, which Isabelle2008
> already uses to some degree for parallel theory loading.

i would have used Poly/ML right from the start, but I did a Google search for 
{poly ml licence}, which turned up the strange licence at as the first result. Now 
that I've downloaded the latest source, and checked its COPYING file, I see 
that Poly/ML uses the LGPL now, which I'm perfectly happy with. I'll try to 
get going with Poly/ML in the next two or three days.

Thanks for your advice.


Attachment: signature.asc
Description: This is a digitally signed message part.

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