Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] polyml 4.1.3 segfault on debian sid

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: C G <catgame@gmail.com>
On 8/14/05, George Karabotsos <g_karab@cs.concordia.ca> wrote:

I believe this is related to the kernel version of your Debian
installation.

I'm using

/usr/local/polyml-devel-2005.08.15/driver $ uname -a
Linux trtr 2.6.12-1-686 #1 Tue Aug 9 13:00:08 UTC 2005 i686 GNU/Linux

Check this older thread for additional information:
*http://tinyurl.com/7dt4t

Thank you nonetheless!

BTW, I followed the instructions at

http://www.polyml.org/linuxsegfault.html

But it does not help either. I tried a little to build a new ML_dbase
of polyml. But figured I do not have that much time. A lot to learn
right now. :) I'd rather wait for an official fix. :)

Thanks to all you guys!

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: C G <catgame@gmail.com>
I got the following with Isabelle 2004 & polyml 4.1.3
on Debian GNU/Linux sid

/usr/local/polyml-4.1.3/x86-linux $ ./poly
Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002)
Copyright (c) 2002 CUTS and contributors.
Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%)
段错误 (core dumped)

Please help! Thank you!

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: C G <catgame@gmail.com>
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=@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>')

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!

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: George Karabotsos <g_karab@cs.concordia.ca>
C G wrote:

I believe this is related to the kernel version of your Debian
installation.

Check this older thread for additional information:
*http://tinyurl.com/7dt4t

*George.

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: C G <catgame@gmail.com>
It seems that I'm running into a never ending series of troubles. When
running ./config/install.sh following INSTALL of smlnj-110.55, I got

...
make[1]: Leaving directory /usr/local/smlnj-110.55/src/runtime/gc' (cd ../mp; make MAKE="make" clean) make[1]: Entering directory /usr/local/smlnj-110.55/src/runtime/mp'
rm -f v-* *.o libmp.a
make[1]: Leaving directory `/usr/local/smlnj-110.55/src/runtime/mp'
/usr/local/smlnj-110.55/config/unpack: Un-GZIP-ing and un-TAR-ing
bootfiles archive.
./config/install.sh: CM metadata directory name is ".cm"
/usr/local/smlnj-110.55/bin/.run/run.x86-linux: Fatal error --
Uncaught exception SysErr with <unknown> raised at <sysconf.c>

./config/install.sh !!! Boot code failed, no heap image (sml.x86-linux).

I've reported this as a bug to smlnj people. Now I'm as far away from
Isabelle as I can be. The good news is that I'm now seriously into the
Isabelle camp. I mean, we really should prove that our programs work!
I see opportunities!

Best wishes

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: George Karabotsos <g_karab@cs.concordia.ca>
C G wrote:

For what is worth, I installed smlnj-110 and use that as my ML base - it
works as well and I have not seen any differences when using the polyml
base at school.

George

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: Dennis Walter <dennis.walter@gmail.com>
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.

Hope this helps.
Cheers,
Dennis

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: Lionel Elie Mamane <lionel@mamane.lu>
I used this patch to driver/configure that made it work. (It also
changes the installation path.)
polyml_opt_debian.patch

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: Martin Ellis <m.a.ellis@ncl.ac.uk>
I never got that package to work with Isabelle.
Instead, I'm just using the latest SML/NJ installed from sources.

Martin

view this post on Zulip Email Gateway (Aug 17 2022 at 13:26):

From: C G <catgame@gmail.com>
Thanks! It works!

Last updated: May 03 2024 at 04:19 UTC