Email Gateway (Aug 18 2022 at 10:41): Email Gateway (Aug 18 2022 at 10:41):From: Dominic Mulligan <s0346804@sms.ed.ac.uk>
Hi all,
I'm attempting to use a CVS version of Isabelle with polyml-5.0. When
I try to start the Isabelle process from the command line ("isabelle" or
"isabelle-process") Isabelle refuses to start and I get the following
error: "Unable to allocate immutable area" (incidentally, I also get
this error when trying to build the heaps, I'm currently using a heap
built on another machine). Trying to start Isabelle from within PG also
gives a similar error (this time preceded by a warning about locales,
first line of error: "perl: Setting locale failed", then followed by
warnings stating my locale is being set to the standard locale, ("C"),
and finally the error about the immutable area).
I have tried to use polyml-4.2 (the version linked to on the Isabelle
site) to build the HOL heap, but after a build time of over an hour and
a quarter, I gave up. Clearly something is seriously wrong. For my
purposes, I'd like to stick with the version of Isabelle that I'm trying
to use. With this in mind, can anyone shed any light on the origin of
the "unable to allocate immutable area" error, and what can be done to
fix it? A quick Google search has turned up nothing of note.
Many thanks,
Dominic Mulligan.
Email Gateway (Aug 18 2022 at 10:41):From: Makarius <makarius@sketis.net>
This sounds like a genuine problem of Poly/ML on your particular platform,
although 5.0 usually works quite well on a large number of systems.
Maybe you should ask on the polyml mailing list.
Makarius
Last updated: May 03 2024 at 04:19 UTC