Email Gateway (Aug 22 2022 at 10:56): Email Gateway (Aug 22 2022 at 10:56):From: Ramana Kumar <rk436@cam.ac.uk>
Hi,
I am trying to run Sledgehammer on Isabelle2015. Whenever I try, I get this
error message:
Welcome to Isabelle/HOL (Isabelle2015: May 2015)
poly: loadlocale.c:130: _nl_intern_locale_data: Assertion `cnt < (sizeof
(_nl_value_type_LC_COLLATE) / sizeof (_nl_value_type_LC_COLLATE[0]))'
failed.
/home/ramana/Isabelle2015/lib/scripts/run-polyml-5.5.2: line 82: 16420
Aborted (core dumped) "$POLY" -q -i $ML_OPTIONS --eval
"$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit <
/dev/null
message_output terminated
standard_output terminated
standard_error terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134
I have no idea how to debug this. What could be wrong?
Thanks,
Ramana
Email Gateway (Aug 22 2022 at 10:56):From: Ramana Kumar <rk436@cam.ac.uk>
Mark,
Thanks for the link. That link suggests there is an issue with requiring
32-bit versions of glibc. I thought Isabelle2015 runs natively on a 64-bit
machine. Am I incorrect about that?
(I haven't tried installing lib32-glibc yet, because I suspect it's not
necessary. I will try it later, though, to test.)
Thanks,
Ramana
Email Gateway (Aug 22 2022 at 10:56):From: Makarius <makarius@sketis.net>
Isabelle2015 consists of many components. This thread is about the "poly"
process, i.e. the Poly/ML runtime process. Running that "natively" on
x86_64 works, but wastes a lot of resources. The usual way is to install
32-bit C/C++ standard libraries, what ever that means concretely on
particular Linux distributions.
Gladly, users on Windows and Mac OS X don't have to think about such
side-conditions.
Makarius
Email Gateway (Aug 22 2022 at 10:57):From: Ramana Kumar <rk436@cam.ac.uk>
On 22 August 2015 at 17:49, Makarius <makarius@sketis.net> wrote:
Isabelle2015 consists of many components. This thread is about the "poly"
process, i.e. the Poly/ML runtime process. Running that "natively" on
x86_64 works, but wastes a lot of resources. The usual way is to install
32-bit C/C++ standard libraries, what ever that means concretely on
particular Linux distributions.
In case it helps anyone else: installing the 32-bit version of glibc did
indeed fix the problem.
Gladly, users on Windows and Mac OS X don't have to think about such
side-conditions.
Perhaps, but instead they have to worry about using proprietary software
and all that that entails.
Email Gateway (Aug 22 2022 at 10:57):From: Makarius <makarius@sketis.net>
I am using mostly Linux myself, but in a way to avoid problems.
The Isabelle system integration we see today makes the system run out of
the box for 99% percent of users, but 1% need extra tinkering, or don't
manage at all.
In the worst case, it is always possible to run Virtualbox with Windows or
plain Ubuntu, even on exotic Linux distributions.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC