Re: [isabelle] Problem running Isabelle on Sparc/Solaris
Paul Hachmann wrote:
I am also using this solution with exactly the same sml/nj version and
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.
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
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
(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.
@Paul: Does the stop-button work for you ?
Greetings and thanks for your hints
This archive was generated by a fusion of
Pipermail (Mailman edition) and