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 gmail.com> wrote:
> 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:
> 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_OPTIONS=-H 200
> ISABELLE_USEDIR_OPTIONS=-M max -p 1 -q 2 -v true -V outline=/proof,/ML
> And the error:
> make: 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
> Installing HOL_x86-linux.tar.gz from the instructions for Isabelle-2009-1
> does not appear to help either.
> Any suggestions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and