Re: [isabelle] Errors when installing and executing Isabelle-2009-2
On Sun, 9 Jan 2011, John Nicol wrote:
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!
On Sun, Jan 9, 2011 at 7:58 PM, Thomas Sewell <Thomas.Sewell at nicta.com.au>wrote:
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and