Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Segmentation faults when running PolyML


view this post on Zulip Email Gateway (Aug 18 2022 at 10:40):

From: Ricardo Peña <ricardo@sip.ucm.es>
Hello,

I am copying below part of the message from Ewen Maclean on 19.10.2005:

I noticed in the archives many problems reporting the segmentation
fault with the latest polyml.
I managed to get isabelle to build with polyml 4.1.4 by using the
4.1.4 driver and the 4.1.3 database.
I am including these in case anyone is still having problem building
Isabelle,
or is unfamiliar with building polyml from source.
This worked for me to get Isabelle working so here are the steps:
(I am assuming the x86 architecture - hence the i386, but it can be
done for others)

I have followed all the steps described there, but when I type:

poly ML_dbase < mlsource/BuildAll.sml

I get segmentation fault, as well as when executing the binaries of the
original distribution. I am using Linux Debian, and this is the
information I get with the command 'uname -a':

Linux 2.6.17-1-686 #1 SMP Fri Jun 23 17:38:22 UTC 2006 i686 GNU/Linux

Can anybody help to fix this?

Thanks

Ricardo

view this post on Zulip Email Gateway (Aug 18 2022 at 10:41):

From: Makarius <makarius@sketis.net>
These problems may be avoided altogether by using Poly/ML 5.0. See also
http://www4.in.tum.de/~wenzelm/test/Isabelle2005-polyml-5.0.tar.gz on how
to make it work with Isabelle2005.

The latest CVS version of Poly/ML should also work, but make double sure
that Isabelle sees ML_SYSTEM=polyml-5.0, not 5.1 as reported by Poly/ML.

Makarius


Last updated: May 03 2024 at 08:18 UTC