Email Gateway (Aug 18 2022 at 16:54): Email Gateway (Aug 18 2022 at 16:54):From: John Nicol <nicol.john@gmail.com>
Hello,
I am on Ubuntu 10.10, with Perl 5.10.1 and Java 1.6.0_22.
After following the Linux instructions at
http://www.cl.cam.ac.uk/research/hvg/Isabelle/download.html and running
running /usr/local/Isabelle/bin/
isabelle/tty, I get the following errors:
env: /usr/local/Isabelle2009-2/contrib/polyml/x86-linux/poly: No such file
or directory
Unknown logic "HOL" -- no heap file found in:
/home/jnicol/.isabelle/heaps/Isabelle2009-2/polyml_x86-linux
/usr/local/Isabelle2009-2/heaps/polyml_x86-linux
But /usr/local/Isabelle2009-2/contrib/polyml/x86-linux/poly exists, and has
execution rights? I looking for solutions online, and found suggestions to
install HOL, or to build Isabelle, neither of which seem to help.
isabelle/build output:
ML_SYSTEM=polyml
ML_HOME=/usr/local/Isabelle2009-2/contrib/polyml/x86-linux
ML_OPTIONS=-H 200
ML_PLATFORM=x86-linux
ISABELLE_USEDIR_OPTIONS=-M max -p 1 -q 2 -v true -V outline=/proof,/ML
And the error:
make[1]: Entering directory `/usr/local/Isabelle2009-2/src/Pure'
Building Pure ...
Pure FAILED
(see also /usr/local/Isabelle2009-2/heaps/polyml_x86-linux/log/Pure)
/usr/local/Isabelle2009-2/lib/scripts/run-polyml: line 74:
/usr/local/Isabelle2009-2/contrib/polyml/x86-linux/poly: No such file or
directory
Installing HOL_x86-linux.tar.gz from the instructions for Isabelle-2009-1
does not appear to help either.
Any suggestions?
Thanks!
John
Email Gateway (Aug 18 2022 at 16:54):From: John Nicol <nicol.john@gmail.com>
Installing Adobe Flash (which depends on some of the libc libraries) appears
to have fixed the problem. It reconfigured libc6-i386 and lib32stdc++6 and
some other libraries.
I assume this is related to this problem, although the error was less
clear:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-March/msg00003.html
I'd recommend listing the libc dependencies on the installation page and/or
putting a descriptive error in the code. This was a fairly clean Ubuntu
installation, so I'm sure this problem will pop up again.
Thanks,
John
Email Gateway (Aug 18 2022 at 16:54):From: Alexander Krauss <krauss@in.tum.de>
John Nicol wrote:
In fact, a student at TUM recently had what seems to be exactly the same
problem. It was also a more or less clean Ubuntu installation. We could
not solve it at that time, and it somehow went away after he reinstalled
the system.
So it may be a not-so uncommon error.
Alex
Email Gateway (Aug 18 2022 at 16:54):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
This might be an instance of a problem we've seen frequently, where a 32-bit binary is executed on a 64-bit linux which doesn't have ia32libs installed. I think the problem is not even a missing dynamic library but a failure to find the dynamic linking program which is usually named as an interpreter, and the error comes from the kernel itself. I might be mistaken. Anyway, there's no easy way to change the unhelpful error message without wrapping the executable in yet another script.
Yours,
Thomas.
Email Gateway (Aug 18 2022 at 16:54):From: John Nicol <nicol.john@gmail.com>
Yes, I'm on 64-bit, and I see in the logs that ia32libs was in the install
that fixed the error. Good call. Would be a great FAQ entry!
Cheers,
John
Email Gateway (Aug 18 2022 at 16:54):From: Lars Noschinski <noschinl@in.tum.de>
Yep, this is due to missing dynamic linker (/lib/ld-linux.so.2). On
Debian-based systems, this file is part of libc6-i386. ia32libs is not
needed to run Isabelle (but depends on libc6-i386, so it will fix the
symptons).
On Fedora, bash contains code to detect a missing dynamic linker, but
this seems to be quite involved[1]; so not worth to be added to Isabelle.
[1] http://kerneltrap.org/mailarchive/linux-kernel/2010/3/27/4552425
Email Gateway (Aug 18 2022 at 16:55):From: Makarius <makarius@sketis.net>
I've had the same when installing my own system 64bit laptop more than a
year ago, but assumed that people doing such things would know the tricks.
Anyway, the deeper reason for the confusion here is that the failure to
execute "poly" is essentially ignored, and an unexpected directory for the
logic images is produced instead. I have now simplified our historic ML
autoconfiguration a bit, to get rid of such features in the coming
release: Isabelle2011 with Poly/ML 5.4.0 from our download site. Stay
tuned ...
Makarius
Email Gateway (Aug 18 2022 at 16:55):From: Timothy McKenzie <tjm1983@gmail.com>
I think this error is probably what led me to get Isabelle running
in 64-bit mode on my 64-bit Fedora laptop. I think I concluded
that 64-bit Linux required 64-bit Isabelle, but now it seems that
I might be able to get it running in 32-bit mode by installing
glibc.i686. Is there any benefit in doing so, now that I've
already got 64-bit Isabelle up and running?
Timothy
<><
signature.asc
Email Gateway (Aug 18 2022 at 16:55):From: Alexander Krauss <krauss@in.tum.de>
Hi Timothy,
The memory footprint of 32-bit Isabelle is significantly smaller, due to
the more compact representation of pretty much everything. So I think
the standard approach is to only use 64-bit when your applications hit
the address space barrier of 4GB. This is what used to be the 640kB
barrier not long ago :-)
Alex
Email Gateway (Aug 18 2022 at 16:55):From: Timothy McKenzie <tjm1983@gmail.com>
Thanks. I got 32-bit Isabelle to work on 64-bit Fedora 13 by
commenting out the 64-bit-specific things I'd put in my
~/.isabelle/etc/settings file, installing glibc.i686 (for /lib/ld-
linux.so.2) and libstdc++.i686 (for /usr/lib/libstdc++.so.6, which
I found was also necessary).
Timothy
<><
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC