Re: [isabelle] RC3 startup problem on Scientific Linux

On Sat, 19 May 2012, Bill Richter wrote:

on a 32-bit Dell PC running Scientific Linux, I got this error when running (localhost)Isabelle2012-RC3> ./Isabelle 6Tarski.thy&

A window popped up with the title
Failed to start Isabelle process
and the window said:

/home/richter/Isabelle2012-RC3/contrib/polyml/x86-linux/poly: /lib/ version `GLIBC_2.7' not found (required by /home/richter/Isabelle2012-RC3/contrib/polyml/x86-linux/poly)

Which version of Scientific Linux do you have?

Which version of libc is it?  E.g. what is the symlink:

  $ ls -al /lib/
  /lib/ ->  # Ubuntu 10.04 LTS

I click OK and then I see my file 1Tarski.thy displayed in jedit, but with none of the highlighting and font changes I see when I run it in regular Isabelle. Everything is fine there except for the do-not-enter for the first line.

The "Prover Session / Syslog" should tell you more about the status of the prover process -- or its startup failure.

Now on a 64-bit Dell PC running Scientific Linux, jedit didn't even
come up, and I got this error message:

(poisson)Isabelle2012-RC3> ./Isabelle
11:39:28 PM [main] [error] main: Exception in thread "main"
11:39:28 PM [main] [error] main: java.lang.UnsatisfiedLinkError: /tmp_mnt/rhome/2/richter/Isabelle2012-RC3/contrib/jdk-6u31_x86-linux/jdk1.6.0_31/jre/lib/i386/xawt/ cannot open shared object file: No such file or directory

This means you either need to saturate S.L. x86_64 with more 32-bit libraries -- especially the ones for X11 -- or use the x86_64 version of the Isabelle distribution. There are many binaries in there that work better out-of-the box if the whole thing is native.


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