Email Gateway (Aug 18 2022 at 19:47): Email Gateway (Aug 18 2022 at 19:47):From: Bill Richter <richter@math.northwestern.edu>
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!
Email Gateway (Aug 18 2022 at 19:48):From: Makarius <makarius@sketis.net>
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/libc.so.6: 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/libc.so.6
/lib/libc.so.6 -> libc-2.11.1.so # 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/libmawt.so: libXtst.so.6: 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.
Makarius
Email Gateway (Aug 18 2022 at 19:48):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Makarius! BTW I had this error in RC2 but was too
disorganized to post a bug report. My info here isn't going to be
great, because I'm on the 64-bit machine, but
Which version of Scientific Linux do you have?
I don't know how to figure that out. I tried this:
(poisson)richter> uname -a
Linux poisson.math.northwestern.edu 2.6.32-220.4.1.el6.x86_64 #1 SMP Mon Jan 23 17:20:44 CST 2012 x86_64 x86_64 x86_64 GNU/Linux
Does that say SL version 2.6?
Which version of libc is it? E.g. what is the symlink:
/lib/libc.so.6 -> libc-2.11.1.so # Ubuntu 10.04 LTS
(poisson)richter> ls -al /lib/libc.so.6
lrwxrwxrwx. 1 root root 12 Jan 26 06:11 /lib/libc.so.6 -> libc-2.12.so*
I think it's a glibc problem. The error message was about glibc 2.7,
and I checked: I have glibc 2.5. I can try to install a later rpm.
... use the x86_64 version of the Isabelle distribution.
I'm sorry, I didn't see any such option on
http://isabelle.in.tum.de/website-Isabelle2012-RC3
It just says
Email Gateway (Aug 18 2022 at 19:50):From: Makarius <makarius@sketis.net>
This means you are running 64-bit Linux, and the JavaScript of the website
displays the 64-bit option as a big green download button.
Makarius
Email Gateway (Aug 18 2022 at 19:51):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Makarius, that was dumb of me, to miss the big green button.
Email Gateway (Aug 18 2022 at 19:51):From: Bill Richter <richter@math.northwestern.edu>
This means you are running 64-bit Linux, and the JavaScript of the
website displays the 64-bit option as a big green download button.
It works, Makarius! On the 64-bit Linux, I downloaded the 64-bit
version from http://isabelle.in.tum.de/website-Isabelle2012-RC3, and
it executes both of two good *thy files, and both look fine.
I realized my problem: I thought all links we can click on that are
underlined and have a different font. But I was wrong!
Email Gateway (Aug 18 2022 at 19:53):From: Makarius <makarius@sketis.net>
Excellent.
In the meantime I have also played a bit with your Tarski Geometry in
Isabelle2012. See the included theory file.
For such elementary proofs from a given axiomatization, there is little
more to do for Isar than pasting together facts and rules in the proper
order, sometimes duplicating facts in subtle ways.
"Isar" means "Intelligible semi-automated reasoning": at the bottom there
is no automation built into it, apart from unification. In the
applications you can then add more automated tools explicitly as required.
Makarius
Tarski.thy
Email Gateway (Aug 18 2022 at 19:53):From: Makarius <makarius@sketis.net>
2.6 is the Linux kernel version. From the date it is probably SL 5.x, see
also http://en.wikipedia.org/wiki/Scientific_Linux
Anyway, I have convinced myself that there is nothing special about
Scientific Linux, it is just another RHEL derivative. Current 6.2 works
out of the box with Isabelle2012-RC3.
Note that Wikipedia has this laconic comment on SL:
The name Scientific Linux is actually a misnomer, in that it does not
contain scientific software and was named instead for the labs that make
it.
Makarius
Email Gateway (Aug 18 2022 at 19:53):From: Serguei Mokhov <serguei@gmail.com>
On 5/22/12, Makarius <makarius@sketis.net> wrote:
On Sun, 20 May 2012, Bill Richter wrote:
Which version of Scientific Linux do you have?
I don't know how to figure that out. I tried this:
(poisson)richter> uname -a
Linux poisson.math.northwestern.edu 2.6.32-220.4.1.el6.x86_64 #1 SMP Mon
Jan 23 17:20:44 CST 2012 x86_64 x86_64 x86_64 GNU/LinuxDoes that say SL version 2.6?
Which version of libc is it? E.g. what is the symlink:
/lib/libc.so.6 -> libc-2.11.1.so # Ubuntu 10.04 LTS2.6 is the Linux kernel version. From the date it is probably SL 5.x,
el6 in the uname command tells that it's a SL 6.x variant. To know the
exact version is to:
cat /etc/issue
Judging by the kernel version it is probably 6.1.
see
also http://en.wikipedia.org/wiki/Scientific_LinuxAnyway, I have convinced myself that there is nothing special about
Scientific Linux, it is just another RHEL derivative. Current 6.2 works
out of the box with Isabelle2012-RC3.Note that Wikipedia has this laconic comment on SL:
The name Scientific Linux is actually a misnomer, in that it does not
contain scientific software and was named instead for the labs that make
it.
They did actually package the lab needs specific stuff in the past for
the scientific
software, but that's gone into the extra/external repos, like EPEL,
etc. CERN also
has a its own sub version. Pure SL is indeed an RHEL clone.
I also confirm Isabelle 2012 RC3 works well on SL 6.2 32 bit in this case.
Email Gateway (Aug 18 2022 at 19:53):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Makarius! So I have SL kernel version 6.2.1, and the newer
kernel version 6.2.2 works fine? SL is a RHEL clone built by
FermiLab, with the sole advantage that it doesn't cost anything. Red
Hat started charging $$, so the NWU Math dept switched to SL.
Last updated: Apr 25 2024 at 20:15 UTC