Email Gateway (Aug 18 2022 at 12:48): Email Gateway (Aug 18 2022 at 12:48):From: Tim McKenzie <tjm1983@gmail.com>
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 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.
Tim
<><
Pure
signature.asc
Email Gateway (Aug 18 2022 at 12:48):From: Makarius <makarius@sketis.net>
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
Poly/ML.
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
http://isabelle.in.tum.de/polyml-5.2.1/
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_PLATFORM=x86-linux
ML_HOME="/home/polyml/polyml-5.2.1/$ML_PLATFORM"
ML_SYSTEM=polyml-5.2
ML_OPTIONS="-H 500"
Here ML_SYSTEM is the critical bit.
Makarius
README
Email Gateway (Aug 18 2022 at 12:48):From: Tim McKenzie <tjm1983@gmail.com>
On Wednesday 31 December 2008 01:18:24 Makarius wrote:
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
http://www.lfcs.inf.ed.ac.uk/software/polyml/Get.html 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.
Tim
<><
signature.asc
Last updated: May 03 2024 at 04:19 UTC