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>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 tuned ...


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.