Email Gateway (Aug 22 2022 at 15:56): Email Gateway (Aug 22 2022 at 15:56):From: Makarius <makarius@sketis.net>
I am surprised that the above did work with Isabelle2016-1 -- apparently
by accident.
When you unpack as root, the permissions are usually taken from the
tar.gz and are thus somewhat erratic. If we assume that everything is
nicely normalized to root, e.g. via "chmod -R root:root" on the
resulting ISABELLE_HOME directory, a non-root user should not be able to
write into ISABELLE_HOME/heaps as is required when starting the main
application (this is due to the built-in "isabelle build -s").
I've tried this briefly on my Ubuntu 16.04.2 LTS, and it works uniformly
as expected, i.e. cannot start the unpacked Isabelle application because
the heap directory cannot be created by non-root.
Of course, you should never run huge application agglomerates like
Isabelle as root. Instead it should work like this:
* Unpack and run the application as non-root in some arbitrary user
directory.
* Copy the result as root, e.g. "cp -R Isabelle2016-1 /opt"
Option -R is sufficient to preserve potential symlinks but normalizes
all permissions and owner in the standard way for root.
Afterwards it should be possible for any user to run the application
from /opt. If that user is only you, you can actually skip the
copy-to-/opt part altogether and keep things in a regular user
directory. This scheme has the advantage that the system can be
exchanged underneath without having to put the application back in place
afterwards.
Another note: I see polyml-5.6_x86_64-linux above, but for most
practical purposes the x86-linux version performs better. You merely
need to ensure that the 32-bit C/C++ standard libraries are installed.
Makarius
Email Gateway (Aug 22 2022 at 15:56):From: Dominique Unruh <unruh@ut.ee>
Dear all,
when I install Isabelle (unpacking the Linux archive into /opt) as root,
and then run Isabelle a non-root using
"/opt/Isabelle2017-RC0/Isabelle2017-RC0", jedit starts up, but brings a
dialog box with the following error message:
Failed to create directory:
"/opt/Isabelle2017-RC0/heaps/polyml-5.6_x86_64-linux/log"
In 2016-1, it was possible to install and run Isabelle this way.
If I make /opt/Isabelle2017-RC0 readwrite for the non-root user, everything
works.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 15:57):From: Dominique Unruh <unruh@ut.ee>
I am surprised that the above did work with Isabelle2016-1 -- apparently
by accident.
Neither does it for me, now. But I think I figured out what it was that
confused me.
If I perform the following steps:
However, if I perform the following steps:
Thus the two ways of invoking jEdit have different defaults, which is
confusing, I think.
(Also, I couldn't find documentation for the
/opt/Isabelle2017-RC0/Isabelle2017-RC0 executable to see what the defaults
are.)
Another note: I see polyml-5.6_x86_64-linux above, but for most
practical purposes the x86-linux version performs better. You merely
need to ensure that the 32-bit C/C++ standard libraries are installed.
I installed the package "libc6-i386" in Ubuntu 17.04. (Via the normal "sudo
apt install libc6-i386".) Isabelle still uses x64 by default.
Best wishes,
Dominique.
When you unpack as root, the permissions are usually taken from the
tar.gz and are thus somewhat erratic. If we assume that everything is
nicely normalized to root, e.g. via "chmod -R root:root" on the
resulting ISABELLE_HOME directory, a non-root user should not be able to
write into ISABELLE_HOME/heaps as is required when starting the main
application (this is due to the built-in "isabelle build -s").I've tried this briefly on my Ubuntu 16.04.2 LTS, and it works uniformly
as expected, i.e. cannot start the unpacked Isabelle application because
the heap directory cannot be created by non-root.Of course, you should never run huge application agglomerates like
Isabelle as root. Instead it should work like this:* Unpack and run the application as non-root in some arbitrary user
directory.* Copy the result as root, e.g. "cp -R Isabelle2016-1 /opt"
Option -R is sufficient to preserve potential symlinks but normalizes
all permissions and owner in the standard way for root.Afterwards it should be possible for any user to run the application
from /opt. If that user is only you, you can actually skip the
copy-to-/opt part altogether and keep things in a regular user
directory. This scheme has the advantage that the system can be
exchanged underneath without having to put the application back in place
afterwards.Another note: I see polyml-5.6_x86_64-linux above, but for most
practical purposes the x86-linux version performs better. You merely
need to ensure that the 32-bit C/C++ standard libraries are installed.Makarius
Email Gateway (Aug 22 2022 at 15:57):From: Makarius <makarius@sketis.net>
On 29/08/17 10:18, Dominique Unruh wrote:
If I perform the following steps: * Install read-only in /opt * Run /opt/Isabelle2017-RC0/Isabelle2017-RC0
Then I get the error (because the build process is invoked with -s, I
guess).However, if I perform the following steps: * Install read-only in /opt * Run /opt/Isabelle2017-RC0/bin/isabelle jedit
Then building proceeds (with heaps in ~/.isabelle)Thus the two ways of invoking jEdit have different defaults, which is
confusing, I think.
(Also, I couldn't find documentation for the
/opt/Isabelle2017-RC0/Isabelle2017-RC0 executable to see what the
defaults are.)
The latter is occasionally called "main Isabelle desktop application",
but not documented further. It is the first thing that most users
encounter and usually run on the spot. Thus the default logic image will
become part of the application directory (due to the implicit -s option
that is only documented as part of "isabelle jedit" in the "jedit"
manual, "isabelle build" in the "system manual).
Very few people ever notice these fine points, which is an indication
that it usually works without further ado.
The extra aspect of read-only installation in a system directory has
always been morally supported, but is seen extremely rarely these days,
and system administrators usually get it wrong one way or the other.
Maybe I should write a note how to do it in the manual, so that I can
point to that next time.
Another note: I see polyml-5.6_x86_64-linux above, but for most
practical purposes the x86-linux version performs better. You merely
need to ensure that the 32-bit C/C++ standard libraries are installed.I installed the package "libc6-i386" in Ubuntu 17.04. (Via the normal
"sudo apt install libc6-i386".) Isabelle still uses x64 by default.
On Ubuntu the relevant library packages contain the name "multilib",
e.g. "g++-multilib" or "g++5-multilib". I never know which ones are
really required (this is also changing over the years), but merely
install some of them at will until the 32bit "poly" executable works.
Makarius
Email Gateway (Aug 22 2022 at 15:57):From: Lars Hupel <hupel@in.tum.de>
More specifically, you can install lib32stdc++6 on Ubuntu (both 14.04 and 16.04 IIRC) and get just the required library.
Cheers
Lars
Last updated: Apr 25 2024 at 08:20 UTC