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



On Thu, 1 Mar 2007, Peter Lammich wrote:

> [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")"

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





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