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



On Wed, 2007-07-03 at 15:21 +0100, Peter Lammich 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

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.

Hope that helps.

-- 
Fare thee well,
Paul `Satoshi' Hachmann






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