Email Gateway (Aug 28 2023 at 07:12): Email Gateway (Aug 28 2023 at 07:12):From: Frederik Krogsdal Jacobsen <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
While trying Isabelle2023-RC4, I noticed a "bug"/dependency which has
been present since Isabelle2023-RC0.
I apologize for not catching this earlier, but I was out of office until
recently.
The issue seems to have surfaced after commit eaf234b0c849, which moves
the detection of the ISABELLE_HOSTNAME variable from a bash call in
Scala to a bash script.
The detection is implemented using the command "hostname -s" which on
Linux is provided by the inetutils package. Since this package was not
installed on my system, the script halts at that line, which for me
manifested as follows: when I open Isabelle/jEdit, the GUI comes up, but
the prover never starts, and I get a popup saying: "Undefined Isabelle
environment variable: "ISABELLE_HOSTNAME"" and a terminal line saying:
"Isabelle2023-RC4/lib/scripts/getsettings: line 81: hostname: command
not found". This yields Isabelle/jEdit essentially unusable, since no
statements are ever checked by the prover.
In Isabelle2022, where the ISABELLE_HOSTNAME variable is still detected
in Scala, the "hostname -s" command still fails, but this is "caught" by
Scala, and the variable simply ends up being empty.
In any case, the issue is easily fixed by installing inetutils. I don't
know what the ISABELLE_HOSTNAME variable is used for, and Isabelle2022
has worked fine for me even with the variable being empty, though I
guess the previous behaviour of silently ending up with an empty
ISABELLE_HOSTNAME is not intentional.
If the dependency on inetutils is intentional, maybe this should be
noted somewhere (a few Google searches with related keywords did not
yield anything about this issue). The inetutils package mostly contains
clients and servers for obsolete networking protocols, and so it will
probably be more common not to have it installed in the future. The
hostname could perhaps instead be detected by using the command "uname
-n", which should work on all Linux distributions (being part of
coreutils) and macOS.
Thanks,
Frederik
Email Gateway (Aug 28 2023 at 09:20):From: Makarius <makarius@sketis.net>
On 28/08/2023 09:05, Frederik Krogsdal Jacobsen (via cl-isabelle-users Mailing
List) wrote:
The detection is implemented using the command "hostname -s" which on Linux is
provided by the inetutils package.
Which Linux distribution is this actually?
On my Ubuntu 22.04, there is a "required" package called "hostname" that
provides the "hostname" executable.
I find it hard to imagine a version of Linux without "hostname" executable,
but after seeing the ancient "kill" command being effectively killed in 2013,
everything can happen.
The hostname could perhaps instead be
detected by using the command "uname -n", which should work on all Linux
distributions (being part of coreutils) and macOS.
"uname -n" should work, although it lacks the "hostname -s" option.
Makarius
Email Gateway (Aug 28 2023 at 09:54):From: Makarius <makarius@sketis.net>
For the record: the Perl guys are doing it like this in module Sys::Hostname:
https://fastapi.metacpan.org/source/RJBS/perl-5.38.0/ext/Sys-Hostname/Hostname.pm
The source contains many odd comments, but it is often unclear if they should
be taken seriously. For example: "# method 3 - trusty old hostname command"
Makarius
Email Gateway (Aug 28 2023 at 10:54):From: Frederik Krogsdal Jacobsen <cl-isabelle-users@lists.cam.ac.uk>
On 28/08/2023 11:16, Makarius wrote:
Which Linux distribution is this actually?
On my Ubuntu 22.04, there is a "required" package called "hostname"
that provides the "hostname" executable.I find it hard to imagine a version of Linux without "hostname"
executable, but after seeing the ancient "kill" command being
effectively killed in 2013, everything can happen.
I am using Archlinux, and the package I am referring to is GNU
Inetutils, but the situation is relatively common on systemd-based
distributions where the "trusty old" tools have been replaced by
"hostnamectl" and there is no mandatory "legacy" package to provide the
"hostname" command directly like in Ubuntu. Sadly, the syntax for
hostnamectl is not backward compatible, so my best bet is to use "uname"
instead, since this should be available on essentially any Linux system
capable of running Isabelle in the first place.
Alternatively, maybe the JVM has some built-in cross-platform way of
determining the hostname, but I don't know if this is easily available
from Scala.
"uname -n" should work, although it lacks the "hostname -s" option.
I don't know what ISABELLE_HOSTNAME is actually used for, so I have no
comment on whether it is important that ISABELLE_HOSTNAME has some
special format. I imagine that for most users on personal computers, the
hostname is only a single word anyway.
It is certainly also a solution to simply note somewhere that Isabelle
requires that the "hostname" command is available since any reasonable
Linux distribution should have it easily available for installation.
Cheers,
Frederik
Email Gateway (Aug 28 2023 at 11:11):From: Makarius <makarius@sketis.net>
On 28/08/2023 12:54, Frederik Krogsdal Jacobsen wrote:
On 28/08/2023 11:16, Makarius wrote:
Which Linux distribution is this actually?
I find it hard to imagine a version of Linux without "hostname" executable,
but after seeing the ancient "kill" command being effectively killed in
2013, everything can happen.I am using Archlinux, and the package I am referring to is GNU Inetutils, but
the situation is relatively common on systemd-based distributions where the
"trusty old" tools have been replaced by "hostnamectl" and there is no
mandatory "legacy" package to provide the "hostname" command directly like in
Ubuntu.
Thanks for the explanation.
It means that the "hostname" command has been effectively killed as well:
meaning that there is no cross-platform invocation for it that works on common
Linuxes, macOS, Windows/Cygwin.
To address this problem of Linux, I have now made the following change:
https://isabelle.sketis.net/repos/isabelle-release/rev/b96b73a79da3
changeset: 78578:b96b73a79da3
tag: tip
user: wenzelm
date: Mon Aug 28 13:00:24 2023 +0200
files: lib/scripts/getsettings
description:
more robust: "hostname" command might be absent, notably on Arch Linux (and
other systemd-based distributions);
Alternatively, maybe the JVM has some built-in cross-platform way of
determining the hostname, but I don't know if this is easily available from
Scala.
Before using the hostname command, I had checked that already. There is
nothing special in the Java library: it looks all a bit crude and fragile,
compared to what Perl is doing.
I don't know what ISABELLE_HOSTNAME is actually used for, so I have no comment
on whether it is important that ISABELLE_HOSTNAME has some special format. I
imagine that for most users on personal computers, the hostname is only a
single word anyway.
For example, it is used to say which cluster build node runs a job. This is
mainly a "comment" and does not have to be authentic.
Preferably it is an unqualified name that identifies the "node".
(I have derived that "by induction over the current sources", and the
interpretation might change over time.)
Makarius
Last updated: Apr 29 2024 at 01:08 UTC