Re: [isabelle] polyml 4.1.3 segfault on debian sid



On 8/16/05, Dennis Walter <dennis.walter at gmail.com> 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
> (www.smlnj.org) 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.

---------------------8<-------------------------
/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_SYSTEM=smlnj-110
  ML_HOME=/usr/lib/smlnj/bin
  ML_OPTIONS= at SMLdebug=/dev/null
  ML_PLATFORM=x86-linux

  ISABELLE_USEDIR_OPTIONS=-v true


Press RETURN to compilation of

  HOL


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
---------------->8----------------------

Then looking at the log:

-----------------------------8<----------------------
/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
"/root/SML/smlnj-110.52/sml.boot.x86-unix/basis.cm/.cm/x86-unix/basis.cm",
No such file or directory]
  raised at: Basis/Implementation/IO/bin-io-fn.sml:618.25-618.71
             ../cm/util/safeio.sml:30.11
             ../compiler/TopLevel/interact/evalloop.sml:44.55
-
Expected to find ML heap file
/usr/local/Isabelle2004/heaps/smlnj-110_x86-linux/Pure.x86-linux
-------------------------->8------------------------

I was using smlnj package from Debian sid.

--------------------------8<-------------------------
/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
-------------------------->8---------------------------

The relevent part of etc/settings:

--------------------------8<---------------------------
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj-110
#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
ML_HOME=/usr/lib/smlnj/bin
ML_OPTIONS="@SMLdebug=/dev/null"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
---------------------------->8--------------------------

Please help! Thank you!


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