Re: [isabelle] Errors when installing and executing Isabelle-2009-2

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

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.


On Sat, Jan 8, 2011 at 9:10 AM, John Nicol <nicol.john at> wrote:

> Hello,
> I am on Ubuntu 10.10, with Perl 5.10.1 and Java 1.6.0_22.
> After following the Linux instructions at
> 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_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 ...
> (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

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