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



> 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:
* 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.)

> 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
>



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