Email Gateway (Aug 19 2022 at 12:19): Email Gateway (Aug 19 2022 at 12:19):From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi,
Local support is trying to install Isabelle 2013 (prior to current release) on 64bit
machines running Fedora (Linux). This is to use Isabelle for undergraduates at Newcastle.
Isabelle 2012 / 13 used to work before on these workstations. The department
improved all lab machines to become 64 bits, and now, after installing Isabelle again,
support tells me they are getting this:
"
bash-4.2$ isabelle jedit
/usr/local/Isabelle/2013/lib/Tools/java: line 6: /usr/local/Isabelle/2013/contrib/jdk-7u13/x86_64-linux/jdk1.7.0_13/bin/java: No such file or directory
"
Any suggestion on what is the problem or how to fix it?
Many thanks
Leo
Email Gateway (Aug 19 2022 at 12:19):From: Makarius <makarius@sketis.net>
On Mon, 7 Oct 2013, Leo Freitas wrote:
The department improved all lab machines to become 64 bits, and now,
after installing Isabelle again, support tells me they are getting this:"
bash-4.2$ isabelle jedit
Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)
Using bulky 64bit version of Poly/ML instead
This is just a warning: it can be avoided by installing libc++ etc. for
x86 -- I think Fedora calls this platform variant "i686".
/usr/local/Isabelle/2013/lib/Tools/java: line 6: /usr/local/Isabelle/2013/contrib/jdk-7u13/x86_64-linux/jdk1.7.0_13/bin/java: No such file or directory
"
The question here is what happended to
contrib/jdk-7u13/x86_64-linux/jdk1.7.0_13 -- maybe that directory was just
deleted by some admin guy.
In Isabelle2013 and Isabelle2013-1, the Linux bundles for Isabelle should
work uniformly on x86 and x86_64. The difference is how Poly/ML is run,
and which heap images are produced.
Also note that for this slightly old-fashioned scenario of central
installation, the required logic images should be produced once after
installation like this:
/usr/local/Isabelle/2013/bin/isabelle build -b -s HOL
These days the success rate is much higher by letting students download
and run the system directly on their own machines, and bypass "lab"
machines.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC