[isabelle] RC3 startup problem on Scientific Linux



Makarius, 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/libc.so.6: version `GLIBC_2.7' not found (required by /home/richter/Isabelle2012-RC3/contrib/polyml/x86-linux/poly)
/home/richter/Isabelle2012-RC3/contrib/polyml/x86-linux/poly: /lib/libc.so.6: version `GLIBC_2.7' not found (required by /home/richter/Isabelle2012-RC3/contrib/polyml/x86-linux/libgmp.so.3)
Return code: 127

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.

theory 6Tarski
imports Main 
begin

locale tarski-first7 =
fixes C :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool" (- - \<equiv> - - [99,99,99,99] 50)
fixes B :: 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool
assumes A1: "\<forall> a b. a b \<equiv> b a"
 and A2: "\<forall> a b p q r s. a b \<equiv> p q \<and> a b \<equiv> r s =\<Rightarrow> p q \<equiv> r s"
 and A3: "\<forall> a b c. a b \<equiv> c c =\<Rightarrow> a = b"
 and A4: "\<forall> q a b c. \<exists> x. B q a x \<and> a x \<equiv> b c"
 and A5: "\<forall> a b c d a' b' c' d' . not(a = b) \<and> B a b c \<and> B a' b' c'
              \<and> a b \<equiv> a' b' \<and> b c \<equiv> b' c' \<and> a d \<equiv> a' d' \<and> b d \<equiv> b' d'
                        =\<Rightarrow> c d \<equiv> c' d'"
 and A6: "\<forall> a b. B a b a =\<Rightarrow> a = b"
 and A7: "\<forall> a b c p q. B a p c \<and> B b q c =\<Rightarrow> \<exists> x. B p x b \<and> B q x a"

end


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/libmawt.so: libXtst.so.6: cannot open shared object file: No such file or directory
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader$NativeLibrary.load(Native Method)
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1807)
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1703)
11:39:28 PM [main] [error] main:  at java.lang.Runtime.load0(Runtime.java:770)
11:39:28 PM [main] [error] main:  at java.lang.System.load(System.java:1003)
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader$NativeLibrary.load(Native Method)
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1807)
11:39:28 PM [main] [error] main:  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1724)
11:39:28 PM [main] [error] main:  at java.lang.Runtime.loadLibrary0(Runtime.java:823)
11:39:28 PM [main] [error] main:  at java.lang.System.loadLibrary(System.java:1028)
11:39:28 PM [main] [error] main:  at sun.security.action.LoadLibraryAction.run(LoadLibraryAction.java:50)
11:39:28 PM [main] [error] main:  at java.security.AccessController.doPrivileged(Native Method)
11:39:28 PM [main] [error] main:  at sun.awt.NativeLibLoader.loadLibraries(NativeLibLoader.java:38)
11:39:28 PM [main] [error] main:  at sun.awt.DebugHelper.<clinit>(DebugHelper.java:29)
11:39:28 PM [main] [error] main:  at java.awt.Component.<clinit>(Component.java:566)
11:39:28 PM [main] [error] main:  at org.gjt.sp.jedit.GUIUtilities.showSplashScreen(GUIUtilities.java:1810)
11:39:28 PM [main] [error] main:  at org.gjt.sp.jedit.jEdit.main(jEdit.java:339)
(

However, Proof General came up, with 

(poisson)Isabelle2012-RC3> bin/isabelle emacs ../Isabelle/6Tarski.thy 

But when I clicked the button process whole buffer, I got the error message

I can't find any complete commands to process!

-- 
Best,
Bill 





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