Re: [isabelle] Building with SML/NJ
On Tue, 30 Dec 2008, Tim McKenzie wrote:
> I'm trying to build Isabelle's logics from scratch using its built-in
> build script. I go into my Isabelle directory and run:
> ./build Pure
> This fails, and I've attached the resulting log file. I suspect this is
> an SML/NJ bug, but I thought I'd check here first, to see if anyone else
> has encountered this problem. I built SML/NJ 110.68 by running its
> config/install.sh script with the default config/targets file.
I have encountered the same problem when trying 110.68 some weeks ago.
110.67 still works, although it is very big and slow compared to nimble
> I might just download the pre-built logics, but if there's a bug in my
> setup, I still want to get rid of it before it bites again.
Note that everything we provide by default is based on Poly/ML, see also
http://www.polyml.org/ 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.
Recently, parallelism in Isabelle has been improved further -- in the next
release all proofs are checked concurrently. There is also a general
programming ML model based on "futures". Moreover, threads are used for
advanced interaction models, e.g. an improved version of 'sledgehammer'.
In any case, heavy-duty multithreading after Isabelle2008 will require
Poly/ML 5.2.1 for stability reasons, see also
Poly/ML 5.2.1 also works with Isabelle2008 if you pretend it is
polyml-5.2, e.g. like this in etc/settings:
Here ML_SYSTEM is the critical bit.
This distribution of Poly/ML 5.2 has been compiled from the original
sources as follows:
tar xvzf polyml.5.2.tar.gz
chmod +x install-sh
./configure --prefix=/tmp/polyml --without-x
Now /tmp/polyml/bin/* and /tmp/polyml/lib/* are moved to the
platform-specific target directory (e.g. polyml-5.2/x86-linux). Note
that Isabelle/lib/scripts/polyml-platform identifies your platform.
$Id: README,v 1.2 2008/06/03 14:45:59 wenzelm Exp $
This archive was generated by a fusion of
Pipermail (Mailman edition) and