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

On Sat, Jan 8, 2011 at 9:10 AM, John Nicol <nicol.john at gmail.com> 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
> 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
>




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