Re: [isabelle] Isabelle2017-RC0 requires read/write installation



On 28/08/17 13:40, Dominique Unruh wrote:
> 
> 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.

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




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