problems with Isabelle instalation

3 views
Skip to first unread message

Martín Nordio

unread,
Apr 1, 2005, 11:38:26 AM4/1/05
to isabell...@cl.cam.ac.uk
Dear Isabelle users,

I'm Martin Nordio from Rio Cuarto, Argentina and I am learning to use
Isabelle. Isabelle worked very well in my user but not with the others users
of my machine (I have Gentoo Linux). After a few week I updated the system and
now Isabelle does not works for any users.
In both cases, the error is:

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=15000K,ib=3000K,ip=100%,mb=7096K,mp=20%)
/usr/local/Isabelle/bin/../lib/scripts/run-polyml: line 112: 14871
Segmentation fault "$POLY" $ML_OPTIONS "$DB"

Do you know how can I solve this problem? Thanks you for your help.
Best regards

Martin Nordio
Computer Department
National University of Río Cuarto
Argentina


--------
Send messages to isabell...@cl.cam.ac.uk
Conference announcements should be relevant and brief

Martin Ellis

unread,
Apr 1, 2005, 2:21:48 PM4/1/05
to MartínNordio, isabell...@cl.cam.ac.uk
On Friday 01 Apr 2005 17:02, Martín Nordio wrote:
> I'm Martin Nordio from Rio Cuarto, Argentina and I am learning to use
> Isabelle. Isabelle worked very well in my user but not with the others
> users of my machine (I have Gentoo Linux). After a few week I updated the
> system and now Isabelle does not works for any users.
> In both cases, the error is:
>
> 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=15000K,ib=3000K,ip=100%,mb=7096K,=

mp=20%)
> /usr/local/Isabelle/bin/../lib/scripts/run-polyml: line 112: 14871
> Segmentation fault "$POLY" $ML_OPTIONS "$DB"
>
> Do you know how can I solve this problem? Thanks you for your help.

This was covered on the PolyML list recently, and is due to memory location=
s
that are hardcoded into PolyML being incompatible with recent kernels (my
naive understanding, anyway).
I reported the problem after I upgraded my kernel to 2.6.9.

David Matthews (the PolyML maintainer) said:

> I hadn't had any problems when I tried with the 2.6.9 kernel based on
> the Fedora Core 2 distribution. I had another look at this yesterday
> and tried varying the options for the kernel and finally managed to
> build a kernel which generated the seg fault. It turned out that
> turning OFF the "4GB kernel space and 4 GB user-space virtual memory
> segment" resulted in the seg fault. Maybe this is turned off by default
> in debian. It looks as though this puts some of the libraries into the
> area used by Poly/ML for the local heap.

I've tried this, but still can't get it working. I sent David an email tod=
ay
to clarify which option he means, because the "Processor type and
features->High Memory Support" - which is what I thought he meant -
doesn't seem to work.

Apparently the problem will be fixed in PolyML 4.1.4 (which is still in
development I think), but it wouldn't build Isabelle last time I tried.

Tjark Weber said:
> It's probably something rather trivial though, and
> I'll make sure to keep it in mind when we switch to a new
> version of PolyML for the Isabelle distribution.

I've since reverted to Linux 2.6.8.1 (and hoping I don't need any important=

security patches before Isabelle builds with PolyML 4.1.4).

Hope that helps,
Martin

Reply all
Reply to author
Forward
0 new messages