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/ 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 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:

  ML_OPTIONS="-H 500"

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
  cd polyml.5.2
  chmod +x install-sh
  ./configure --prefix=/tmp/polyml --without-x
  make install

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 MHonArc.