Email Gateway (Aug 23 2022 at 08:34): Email Gateway (Aug 23 2022 at 08:34):From: Makarius <makarius@sketis.net>
This is odd -- I have not seen this before. We need to figure out your
side-conditions for this strange effect.
E.g. you could try to use Isabelle2019/contrib/jdk-11.0.3+7 as replacement for
Isabelle2020-RC1/contrib/jdk-11.0.6+10 --- the latter is referenced here:
Isabelle2020-RC1/lib/scripts/Isabelle_app:exec
"$ISABELLE_HOME/contrib/jdk-11.0.6+10/x86_64-linux/jre/bin/java" \
Isabelle2020-RC1/etc/components:contrib/jdk-11.0.6+10
There are other possibilities. You can try a bisection over the Isabelle
repository. In each step you run:
isabelle components -a && isabelle jedit -f
To ensure that the Prover IDE is properly rebuilt. (More recently that has
become unnecessary, because source content is compared as "shasum" instead of
date stamps.)
Makarius
Email Gateway (Aug 23 2022 at 08:35):From: Makarius <makarius@sketis.net>
Start with a normal Isabelle repository setup according to
https://isabelle-dev.sketis.net/source/isabelle/browse/default/README_REPOSITORY
hg bisect --reset
hg up -r Isabelle2019
#repeat:
isabelle components -a && isabelle jedit -f -l Pure
hg bisect --good #or: --bad
Eventually hg will say "The first bad changeset is ..." (the state so far is
in .hg/bisect-state).
Since a repository clone has slightly different defaults, the problem might be
actually absent even in "hg up -r Isabelle2020-RC1".
Makarius
Email Gateway (Aug 23 2022 at 08:38):From: Peter Lammich <lammich@in.tum.de>
Actually, the problem occurs already in "hg up -r Isabelle2019",
but not in the released Isabelle2019!
It's clearly observable when scrolling with the arrow-down key, e.g.,
over "Pure.thy" ... fluent and at speed of key-repetition rate in
Isabelle2019-RELEASE, and stuttering and much slower than key-rep rate
in Isabelle2019-repository.
Email Gateway (Aug 23 2022 at 08:38):From: Makarius <makarius@sketis.net>
There must be a difference somewhere, probably in your settings, preferences,
properties in $ISABELLE_HOME_USER.
For a repository that is $HOME/.isabelle and for the bundles release
$HOME/.isabelle/Isabelle2019.
Can you make a diff -r on it, with some educated guessing?
Makarius
Email Gateway (Aug 23 2022 at 08:39):From: Peter Lammich <lammich@in.tum.de>
Hi,
I deleted .isabelle, and let an invocation of isabelle jedit (2019
release) generate it again. The problem then occurs also in the
released version.
When I insert
view.antiAlias=subpixel HRGB
into jedit/properties, the problem goes away!
What is the default font rendering, and why does it slow down my
machine so much?
Email Gateway (Aug 23 2022 at 08:39):From: Peter Lammich <lammich@in.tum.de>
This also fixes the problem for Isabelle-2020-RC1.
Email Gateway (Aug 23 2022 at 08:39):From: Makarius <makarius@sketis.net>
Interesting observation.
What is your precise Linux version, desktop environment, graphics hardware?
The antialising default has fluctuated many times in the history of jEdit and
Isabelle/jEdit, but "standard" works best on most machines that I have seen
most of the time.
Here are some notable points in history:
jEdit repository:
r22917 | ezust | 2013-04-04 22:34:59 +0200 (Thu, 04 Apr 2013) | 2 lines
Enable subpixel antialiasing by default in textarea.
Isabelle/jEdit repository:
changeset: 70081:093ab1a99eb6
user: wenzelm
date: Tue Apr 09 10:28:17 2019 +0200
files: src/Tools/jEdit/src/jEdit.props
description:
back to more robust "standard" anti-aliasing (reverting f610115ca3d0):
sub-pixel rendering can have odd color effects, even on high-end displays;
changeset: 69798:f610115ca3d0
user: wenzelm
date: Sun Feb 10 19:07:53 2019 +0100
files: src/Tools/jEdit/src/jEdit.props
description:
enable subpixel anti-aliasing by default, assuming that its 4 variants don't
make a difference;
changeset: 34334:68e172602b86
user: wenzelm
date: Tue Oct 21 21:48:44 2008 +0200
files: src/Tools/jEdit/dist-template/properties/jedit.props
description:
essential default properties for jEdit;
Makarius
Email Gateway (Aug 23 2022 at 08:40):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the official Isabelle2020 release is scheduled for the week of 15-Apr-2020, so
we have more than 6 weeks for testing release candidates. Afterwards
everything remains final and unchanged until the next release 8-10 months later.
The blog entry
https://isabelle-dev.sketis.net/phame/post/view/5/release_candidates_for_isabelle2020
is dynamically updated to follow the release process.
The main website is https://isabelle.in.tum.de/website-Isabelle2020-RC1
When discussing observations about Isabelle2020 release candidates on the
mailing list, please provide a "Subject:" line that fits to the content, not
just a clone of this announcement.
Makarius
Email Gateway (Aug 23 2022 at 08:46):From: Peter Lammich <lammich@in.tum.de>
Hi List,
here's my experience report from porting two medium-sized projects,
namely isafol/GRAT/gratchk and Isabelle-LLVM. The former was ported
from Isabelle-2018, the latter from 2019. Porting went smooth and took
less time than expected, only about 1.5h for both.
Last updated: Apr 19 2024 at 08:19 UTC