Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem running Isabelle on Sparc/Solaris

view this post on Zulip Email Gateway (Aug 18 2022 at 10:16):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Makarius wrote:

polyml-5.0 seems not much better, the make-process of polyml-5.0 itself
fails with a segfault:

creating polyimport
./polyimport -H 10 imports/polymlsparc.txt < exportPoly.sml > /dev/null
bash: line 1: 4552 Segmentation Fault ./polyimport -H 10
imports/polymlsparc.txt <exportPoly.sml >/dev/null
*** Error code 139

but I think that is stuff to be solved by the polyml-guys and further
discussion is off-topic for this list. Unfortunately, this error is not
documented in the FAQ, and the
mailing-list archive is restricted, so I have no access to it (unless I
subscribe to the mailing list). Perhaps a polyml-list subscribers can
forward this message there ...

-- Peter Lammich

view this post on Zulip Email Gateway (Aug 18 2022 at 10:17):

From: Paul Hachmann <hachmap@mcmaster.ca>
I had a similar problem a few months ago, so hopefully I can help.

I ended up resolving the problem by recompiling polyml 4.1.4 from source
using smlnj (http://www.smlnj.org/ - I used v110.59). I tried several ML
compilers but this was the only one that worked on Sparc/Solaris
together with polyml and Isabelle.

Then edit .../Isabelle/etc/settings and uncomment the section for sml-nj

Standard ML of New Jersey 110 or later

#SMLNJ_CYGWIN_RUNTIME=1
#ML_SYSTEM=sml
ML_SYSTEM=smlnj-110
#ML_HOME="~/standardML/bin"
ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin"
ML_OPTIONS="@SMLdebug=/dev/null"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")

(Although this may not be optimal...as you can see with the commented
ML_HOME entry I was messing around with compilers a lot and ended up
putting it in a subdirectory of Isabelle itself. I don't remember if
that is required to get it working or not)

Then run the build' script in your Isabelle base directory - it should produce logic heaps in Isabelle/heaps/smlnj-100_sparc-solaris' , which
will then get loaded when you run Isabelle (or proofgeneral) proper. If
it puts them in a directory named `smlnj-100', and Isabelle fails to
find them upon loading, try making the directory yourself and copying
the heaps over :p

Final note: This is with Isabelle2005 - not sure if this works with
anything more recent.

Hope that helps.

view this post on Zulip Email Gateway (Aug 18 2022 at 10:17):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Paul Hachmann wrote:

I am also using this solution with exactly the same sml/nj version and
isabelle2005.
I am using ProofGeneral, and when trying to abort a non-terminating or
long-running proof step via the "stop"-button,
the effect is that the whole isabelle-process dies. This is particular
tedious on longer proof-scripts, because you have to repeat the whole
proof before you can continue.

@Paul: Does the stop-button work for you ?

Greetings and thanks for your hints
Peter Lammich

view this post on Zulip Email Gateway (Aug 18 2022 at 10:17):

From: Paul Hachmann <hachmap@mcmaster.ca>
Hmm..to be honest, I can't recall if I ever used that - I did all my
development on an x86 machine and then ported things over to the Sparc
system, so it already worked :p.

I suspect I would have the same problem as you, though.

view this post on Zulip Email Gateway (Aug 18 2022 at 10:17):

From: Peter Lammich <views@gmx.de>
I want to run Isabelle on a Sparc/Solaris system.
I followed the installation instructions on the website, and then did

[pergolesi] ~/opt $ ./Isabelle/bin/isabelle-process
Poly/ML RTS version Sparc-4.1.4 (14:22:29 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=81920K,ib=16384K,ip=100%,mb=20480K,mp=20%)
Mapping /u/plamm_01/opt/Isabelle2005/heaps/polyml-4.1.4_sparc-solaris/HOL
Mapping /u/plamm_01/opt/Isabelle2005/../polyml/sparc-solaris/ML_dbase
/u/plamm_01/opt/Isabelle2005/lib/scripts/run-polyml: line 126: 22670
Segmentation Fault "$POLY" $ML_OPTIONS "$(fixpath "$DB")"

The same is when I start it from within ProofGeneral.

What can I do now ? Where is the problem and how to fix it ?

Thanks in advance for any help
-- Peter (who has no idea of polyml impl. details or sparc/solaris
architecture)

view this post on Zulip Email Gateway (Aug 18 2022 at 10:21):

From: Makarius <makarius@sketis.net>
What happens when you do this?

./Isabelle/bin/isabelle-process RAW_ML_SYSTEM

Or this?

cd Isabelle/contrib/polyml/sparc-solaris
./poly

Alternatively, you can try polyml-5.0. See
http://www.polyml.org/download.html and
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz

To avoid root access (for /usr/local/bin etc.) you can compile polyml like
this:

./configure --prefix=/tmp/polyml --without-x
make
make install

Then move /tmp/polyml/bin/* and /tmp/polyml/lib/* to
Isabelle/contrib/polyml-5.0/sparc-solaris and make sure
Isabelle/etc/settings find it there.

Makarius

Last updated: May 03 2024 at 08:18 UTC