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



Paul Hachmann wrote:

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
- mine looks like this:

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






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