Re: [isabelle] polyml 4.1.3 segfault on debian sid

On 8/16/05, Dennis Walter < at> wrote:
> I encountered similar problems with Debian Sarge, and the workaround
> for polyml didn't work either. What I did was make SML of New Jersey
> ( the standard ML interpreter by installing it with
> defaults and modifying /path/to/isabelle/etc/settings accordingly
> (simply comment out all polyml related options and uncomment the smlnj
> section). Finally, you just have to recompile the logics you are about
> to use (most notably, HOL), see /path/to/isabelle/INSTALL. This takes
> a while, but is really quite straightforward.

Still no luck.

/usr/local/Isabelle2004 $ ./build

                * Welcome to Isabelle build *

Please check /usr/local/Isabelle2004/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.

The current values are:

  ML_OPTIONS= at SMLdebug=/dev/null


Press RETURN to compilation of


Started at 二  8月 16 10:16:13 CST 2005 (smlnj-110_x86-linux on trtr)
make[1]: Entering directory `/usr/local/Isabelle2004/src/Pure'
Building Pure ...
Finished Pure (0:00:01 elapsed time)
make[1]: Leaving directory `/usr/local/Isabelle2004/src/Pure'
make: *** 没有规则可以创建"/usr/local/Isabelle2004/heaps/smlnj-110_x86-linux/HOL"需要的目标"/usr/local/Isabelle2004/heaps/smlnj-110_x86-linux/Pure"。
Finished at 二  8月 16 10:16:14 CST 2005
0:00:01 total elapsed time

Then looking at the log:

/usr/local/Isabelle2004 $ zcat heaps/smlnj-110_x86-linux/log/Pure.gz
Standard ML of New Jersey v110.52 [built: Fri Jan 21 16:42:10 2005]
!* unable to process `' (unknown extension `<none>')
- [autoloading]

unexpected exception (bug?) in SML/NJ: Io [Io: openIn failed on
No such file or directory]
  raised at: Basis/Implementation/IO/bin-io-fn.sml:618.25-618.71
Expected to find ML heap file

I was using smlnj package from Debian sid.

/usr/local/Isabelle2004 $ sml
Standard ML of New Jersey v110.52 [built: Fri Jan 21 16:42:10 2005]
/usr/local/Isabelle2004 $ dpkg -l|grep smlnj
ii  smlnj                             110.52-1                  
Standard ML of New Jersey interactive compil
ii  smlnj-runtime                     110.52-1                  
Standard ML of New Jersey runtime system

The relevent part of etc/settings:

# Standard ML of New Jersey 110 or later
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")

Please help! Thank you!

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