Email Gateway (Aug 22 2022 at 18:33): Email Gateway (Aug 22 2022 at 18:33):From: Jose Divasón <jose.divasonm@unirioja.es>
I can confirm the problem with linux-image-4.15.0-36-generic in two
different computers. With linux-image-4.15.0-34-generic everything works
well.
In my case, the problem started two days ago (3rd October 2018). I was
working with a file that requires (from AFP)
Perron_Frobenius.HMA_Connect
Rank_Nullity_Theorem.Mod_Type
and Isabelle/jEdit was unable to load the required files and the
corresponding dependences, even waiting for a couple of hours.
Cheers,
Jose
Email Gateway (Aug 22 2022 at 18:33):From: Makarius <makarius@sketis.net>
Here is a test release of Isabelle2018 + a single changeset to avoid
these problems with TCP_NODELAY:
http://isabelle.in.tum.de/Isabelle_05-Oct-2018
The same change is on the ongoing Isabelle development repository:
http://isabelle.in.tum.de/repos/isabelle/rev/6ededdc829bb
Thus Isabelle users on Ubuntu should be able to continue undisturbed.
Next week we will see if Canonical regrets the quite substantial changes
to net/ipv4 of the Linux Kernel, or if that is here to stay. It would be
quite bad indeed: I would have to respin a full Isabelle2018-1 release,
and older releases from the past 5 years would remain unusable.
In the meantime I am still interested to hear about further experience
reports. There is also some chance that Debian has the same problem, or
that it actually originates from Debian.
Makarius
Email Gateway (Aug 22 2022 at 18:33):From: Lars Hupel <hupel@in.tum.de>
Am I right in assuming that this does not affect "isabelle build"?
Email Gateway (Aug 22 2022 at 18:33):From: Makarius <makarius@sketis.net>
Yes, it only affects PIDE sessions, e.g. Isabelle/jEdit, or newer tools
like "isabelle server", "isabelle dump".
Makarius
Email Gateway (Aug 22 2022 at 18:37):From: Makarius <makarius@sketis.net>
After returning from travel and updating my Ubuntu 18.04 LTS
workstation, I still see the same problem with linux-image-4.15.0-34-generic
Ubuntu 18.10 beta appears to work fine. The final release is scheduled
for 18-Oct-2018.
Right now I am inclined to wait for that release, and see if its kernel
also prevents Isabelle/PIDE from working as in the past 5 years.
Are there other Linuxes that are affected to really slow processing of
big sessions in Isabelle/jEdit?
Makarius
Email Gateway (Aug 22 2022 at 18:38):From: Makarius <makarius@sketis.net>
On 13/10/2018 14:30, Makarius wrote:
Next week we will see if Canonical regrets the quite substantial changes
to net/ipv4 of the Linux Kernel, or if that is here to stay. It would be
quite bad indeed: I would have to respin a full Isabelle2018-1 release,
and older releases from the past 5 years would remain unusable.After returning from travel and updating my Ubuntu 18.04 LTS
workstation, I still see the same problem with linux-image-4.15.0-34-generic
Ubuntu 18.10 has been released yesterday, and so far the kernel looks
fine for Isabelle2018.
Ubuntu 18.04.1 LTS is still unchanged: Isabelle/PIDE is unusably slow.
Are there other Linuxes that are affected to really slow processing of
big sessions in Isabelle/jEdit?
Nobody has reported problems for other Linux systems. Only two people
have confirmed the problem for Ubuntu 18.04.1.
For now I am assuming that zero reports really means zero problems on
other Linux systems.
Until the situation becomes worse, e.g. Ubuntu 18.10 other Linux
distributions with non-working kernel, I will not venture on producing
another Isabelle release just to workaround problems on Ubuntu 18.04.1.
Makarius
Email Gateway (Aug 22 2022 at 18:39):From: Peter Lammich <lammich@in.tum.de>
I'm using the LTS versions of Ubuntu ... this thread on the mailing
list has prevented me from upgradig so far, in order to avoid getting
an unusable Isabelle.
So what to do after upgrading, if I need a usable Isabelle2018?
Email Gateway (Aug 22 2022 at 18:40):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
I have the impression that a recent update within the existing Ubuntu
18.04 line causes significant slowdown of socket I/O in Java. This
effect may be seen in the Isabelle Prover IDE when openining a big
session with many sources: it becomes unusably slow.
For now I recommend not to update Ubuntu -- maybe the problem disappears
after a few days by further updates from Canonical.
In the meantime, I continue my experiments to understand the cause for
this problem. I am also grateful to any TCP experts providing helpful
hints, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Pure/System/system_channel.scala
(the socket is later used with read() calls of given lengths).
Makarius
Email Gateway (Aug 22 2022 at 18:40):From: Makarius <makarius@sketis.net>
Or the Isabelle website:
"""
Warning: potential problem with Ubuntu Linux 18.04
The kernel update linux-image-4.15.0-36-generic (Oct-2018) introduces a
timing problem with socket communication in the Isabelle Prover IDE,
notably Isabelle/jEdit. Thus loading big sessions becomes very slow
(e.g. theory HOL-Library.Library or HOL-Analysis.Analysis). This can be
avoided by downgrading to linux-image-4.15.0-34-generic or by using the
following temporary workaround for Isabelle2018.
https://isabelle.in.tum.de/Isabelle_05-Oct-2018/Isabelle_05-Oct-2018_app.tar.gz
"""
Makarius
Email Gateway (Aug 22 2022 at 18:40):From: Makarius <makarius@sketis.net>
Canonical has just published another kernel update for Ubuntu 18.04 LTS:
linux-generic-4.15.0.38.40, and our recent Isabelle versions work again!
So they did regret the deadly change after almost 3 weeks. This probably
also indicates that Ubuntu 18.10 will not acquire the same problem.
Makarius
Email Gateway (Aug 22 2022 at 18:41):From: Makarius <makarius@sketis.net>
The included changeset ch-tcp_delay is a potential workaround for this
potential problem:
changeset: 69119:9380c63aa8cf
tag: tip
parent: 68743:91162dd89571
user: wenzelm
date: Thu Oct 04 16:40:03 2018 +0200
files: src/Pure/General/socket_io.ML
src/Pure/System/system_channel.scala
description:
avoid TCP_NODELAY (in contrast to 18c621069bf8): might cause problems
with some versions of Ubuntu 18.04;
It works for Isabelle2018, but requires a repository clone of that,
instead of a bundled release. This means one needs to follow
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/README_REPOSITORY
and use "hg up -r Isabelle2018" after cloning the repository and before
building anything.
Isabelle users who don't experience any problems with Isabelle/jEdit
performance should not do anything.
I am still unsure what change of Ubuntu 18.04 causes this odd effect: I
have seen it on two machines independently after update. Maybe it is
some bad interaction of defaults for TCP_NODELAY and TCP_QUICKACK. I am
including my own "sysctl -a" diffs for anybody who can read these tea
leaves.
Just by coincidence there will be a Linux TCP code reading session at
Curry Club Augsburg today: https://curry-club-augsburg.de -- maybe I
understand this better afterwards.
Makarius
ch-tcp_delay
sysctl.diff
Email Gateway (Aug 22 2022 at 18:42):From: Makarius <makarius@sketis.net>
The critical package is: linux-image-4.15.0-36-generic
The previous version still works: linux-image-4.15.0-34-generic
Is there anybody who can confirm the problem with Ubuntu Linux Kernel
4.15.0-36? And that it works again after downgrading the package?
The effect is that Isabelle/jEdit socket communication between
Isabelle/ML and Isabelle/Scala is painfully slow, e.g. when opening
$ISABELLE_HOME/src/HOL/Library/Library.thy or
$ISABELLE_HOME/src/HOL/Analysis/Analysis.thy
It can also be avoided by removing the following line in Isabelle/Scala:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Pure/System/system_channel.scala#l29
(but that requires a repository clone of Isabelle2018 to rebuild it
afterwards).
Makarius
Last updated: Apr 23 2024 at 20:15 UTC