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



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





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