Email Gateway (Aug 22 2022 at 19:34): Email Gateway (Aug 22 2022 at 19:34):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the Isabelle2019-RC0/ANNOUNCE file says:
Improved "Isabelle DejaVu" font collection, suitable for text and GUI.
Update to current Java 11 and Poly/ML 5.8 with better scalability.
To clarify this, here are the corresponding NEWS items:
* General *
The font collection "Isabelle DejaVu" is systematically derived from
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif"
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
The DejaVu base fonts are retricted to well-defined Unicode ranges and
augmented by special Isabelle symbols, taken from the former
"IsabelleText" font (which is no longer provided separately). The line
metrics and overall rendering quality is closer to original DejaVu.
INCOMPATIBILITY with display configuration expecting the old
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead.
The Isabelle fonts render "\<inverse>" properly as superscript "-1".
* Isabelle/jEdit Prover IDE *
Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
DejaVu" collection by default, which provides uniform rendering quality
with the usual Isabelle symbols. Line spacing no longer needs to be
adjusted: properties for the old IsabelleText font had "Global Options /
Text Area / Extra vertical line spacing (in pixels): -2", now it
defaults to 0.
OpenJDK 11 has quite different font rendering, with better glyph
shapes and improved sub-pixel anti-aliasing. In some situations results
might be worse than Oracle Java 8, though.
* System *
(There is actually a small mistake above: the line-spacing default is
now 1 instead of 0.)
The change to OpenJDK 11 --- after Java 8 has been officially declared
at "end-of-live" in Jan-2019 --- follows the normal routine of phasing
out old technologies. Moreover, Java 8 had already shown its old age in
Isabelle applications on high-end hardware: it is very inefficient on
machines with many cores (20-80), and does not quite work with
quasi-containers (e.g. Docker). Java 11 solves these and other problems.
It even provides better font rendering, but that requires proper HiDPI
displays (which are commonplace today).
Nonetheless, very nostalgic users may still do their own private
tinkering to return to Java 8 -- even with the old "IsabelleText" font
with its various flaws. I will not support this, though. Big companies
normally provide expensive support plans for continued support of legacy
technologies, but I am not doing this.
Makarius
Email Gateway (Aug 22 2022 at 19:34):From: Makarius <makarius@sketis.net>
One more hint: "Isabelle DejaVu Sans Mono" is still the default for the
main text area, but it is also possible to use the proportional font
"Isabelle DejaVu Sans" instead (or even "Isabelle DejaVu Serif", but
that looks odd to me).
I am not using propertional fonts regularly yet, but have started to
give occasional Isabelle demos with that configuration. After all, the
formal theory text is meant to be a true document, as in LibreOffice or
MS Word (with formal "spell-checking").
The proportional font helps to emphasize this idea, especially to people
who think about proofs as "program code", but also to others who are not
familiar with programming (or "coding").
Makarius
Email Gateway (Aug 22 2022 at 19:34):From: "lammich@in.tum.de" <lammich@in.tum.de>
So what I understand is that Java is phasing out support for proper font
rendering on non UHD screens... Given that many people still use those screens
I somehow can't /don't want to believe that. In particular on laptop screens,
UHD seems not to be standard yet.
Peter
Email Gateway (Aug 22 2022 at 19:34):From: Makarius <makarius@sketis.net>
Please, I have explained the situation so many times.
Strictly speaking, all of Java has been crap all the time. Some brave
guys like the ones behind jEdit have made a great desktop application
from it. I have built on top of that in the past 10 years and will
continue to do so.
Even if Java 11 does demand an up-to-date display now, I cannot really
believe that anybody is still using non-UHD for non-Java things. That is
not rethoric, it is meant seriously. The quality of everyday digital
live changes significantly with it.
(I've been using UHD since Dec-2014, and most high-end Apples were a bit
earlier with "Retina" displays. Now we have Apr-2019.)
Makarius
Email Gateway (Aug 22 2022 at 19:35):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Maybe you should take an interest in the users and in whether "anybody
is still using non-UHD for non-Java things".
To assist you the first reference my quick internet search found is
https://www.tomshardware.com/reviews/monitor-buying-guide,5699.html
entitled "How to Choose a PC Monitor: A 2019 Guide".
Its table of monitor resolutions and what they are called lists 5
resolutions below UHD. Of these the second bottom one is 1920x1080.
Earlier in the article it says "1920x1080, also known as 1080p / Full HD
(FHD) / HD, is the minimum you need". Ie there are four resolutions
equal to or better than its suggested minimum, but below UHD.
Right now I'm looking at a display that is 1366x768. Not what I prefer
to use, but it's what I have when I go travelling. And it (ie the
display as well as the whole machine - CPU, RAM and all) is fine for
using Coq and it's fine for using HOL4 and in fact it's adequate if not
ideal for everything I want to do with it - but it's not much good for
using recent versions of Isabelle. And you shouldn't blame the users
for that
Jeremy
Email Gateway (Aug 22 2022 at 19:35):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
Maybe this problem is not related to the font. Please take a look at my
screenshot: https://pasteboard.co/I8SNpG2.png
I made it on Windows 10 with font scaling set to 125% on the system level.
As you can see icons are big and blurry in Isabelle HOL 2019. Also the font
size is larger.
I guess that it looks blurry because of broken font scaling or dpi settings.
Maybe Isabelle_01-Apr-2019.exe.manifest file is ignored.
сб, 6 апр. 2019 г. в 01:55, Makarius <makarius@sketis.net>:
Email Gateway (Aug 22 2022 at 19:35):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi,
If it is a DPI problem this is not new to Isabelle at all. And it has
nothing to do with Isabelle-2019.
I raised this discussion in a private email with Makarius and Peter, one
and half a year ago.
To sum it up:
To have nice Jedit icons on screens with characteristics (see *section
configuration *below) the use have to:
*override High DPI scaling behavior.
**In Jedit utilities, the user should check Fractional font metrics.
If the use does so, the Jedit icon will be good however the font will be
blurry.
My solution was:
1) Not use () and (*) otherwise I get Blurry font.
2) ignore the tiny and messy Jedit icons on my screen.
You find attached screenshots on Isabelle-2017 and Isabelle-2016-1 which
was as I said one and half a year ago.
section configuration:
I am using a dell XPS 15 with:
-Windows 10 Pro 64-bit OS and x64 based processor.
-For display I have the following drivers:
*Dell- 4 in 1 adapter
*Intel HD graphics 530
*NVIDIA GeForce GTX 960M
Best wishes,
Yakoub
Isabelle2016-1-after-setup.jpg
Isabelle2017-4k.png
Isabelle2016-1-4k.jpg
Email Gateway (Aug 22 2022 at 19:35):From: Makarius <makarius@sketis.net>
Thanks for the hint, I will do some more investigations on Windows 10.
Java 11 does the desktop application integration quite differently from
old Java 8, and there is further potential for problems -- both on
Windows and macOS. I see some other oddities on both platforms that are
absent on Linux, maybe it is due to the builtin scaling as you say.
The slight blur of font-rendering is uniform on all platforms, though.
It is how the OpenJDK font render works (for many years already). Thus
it provides good quality of rendering on good displays, and bad quality
of rendering on bad displays. (The various screenshots of
Isabelle2019-RC0 that have been sent in do mostly look good on my
high-end UHD display that is worth 250 EUR.)
BTW, today I have attended a local conference on Linux and Open-Source:
there was an expert on the KDE desktop environment, one of the guys who
are said to be perfectionistic about visual appearance. He was quite
pleased with the quality of Isabelle2019-RC0 on his full-HD widescreen:
it was old-style but of good quality. Of course, he had a proper UHD
display at home, but was using the old one on the show.
He also agreed with me on imposing DejaVu Sans (not Mono Sans) on the
GUI elements: almost anything apart from the main text area and its
derivates. (And that fine point was actually following the existing
Java/Swing GUI defaults.)
After switching OpenJDK 11 to the GTK+ look-and-feel, he was really
delighted: KDE provides a perfect imitation of itself to the GTK
libraries, so an old-style Swing application looks really great afterwards.
Makarius
Email Gateway (Aug 22 2022 at 19:35):From: Makarius <makarius@sketis.net>
The demand of high-end equipment for high-end applications has been part
of the Isabelle culture from the very beginning.
What we are doing here is the Engineering of Formal Mathematics at a
considerable scale, and it requires a proper Engineering Workstation --
I've just purchased such a beast at 1650 EUR total.
Today there are also mobile versions of that, but the average consumer
model will be insufficient for anything beyond basic examples.
Makarius
Email Gateway (Aug 22 2022 at 19:35):From: Makarius <makarius@sketis.net>
In the meantime, I did most of the work for such a retro-computing
project, see the Isabelle/jEdit manual (changset b718a64d0d09):
:black_small_square: Problem: Font-rendering in Java 11 (OpenJDK) is worse than Java 8
(by Oracle) on low-quality displays.
Workaround: Find an old copy of Java 8 from Oracle (which has
``end-of-live'' status since Jan-2019) and refer to its main directory
via ISABELLE_JDK_HOME="..." in $ISABELLE_HOME_USER/etc/settings. Also
add isabelle_fonts_hints=false to $ISABELLE_HOME_USER/etc/preferences to
avoid problems of the old
font renderer with hinting.
Looking at the Oracle website for Java 8, there is first a big red
warning sign that it is officially at its end-of-live. Poking around a
bit further, one gets the impression that Oracle will provide some
rudimentary security updates for some time to come, for the sake of
corporate users that are still stuck with the old version. (One of these
versions already warn about potential problems with GTK look-and-feel.)
For my part, I don't want to see Java 8 again. I have seen enough
technical problems of Java 8 on high-end server hardware in the past
6-12 months. And the font-rendering of OpenJDK 11 is so much better on
current displays.
Makarius
Email Gateway (Aug 22 2022 at 19:36):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Hi,
What is the problem with having 2 jEdit front ends for PIDE with two
different technologies and see which one is the most downloaded by users?
I think advising student from a country like Algeria to buy hardware for
1600 Eur is a joke.
And not all students are interested nor have the time to hook-up PIDE to
different front-ends to correctly use Isabelle.
Email Gateway (Aug 22 2022 at 19:36):From: Makarius <makarius@sketis.net>
On 07/04/2019 15:43, Nemouchi Yakoub wrote:
What is the problem with having 2 jEdit front ends for PIDE with two
different technologies and see which one is the most downloaded by users?
There is de-facto only one person doing all the system integration and
maintenance. It belongs to my strategy to support only one thing, and
that at a very high quality. Thus I can save a factor 10 of resources.
I think advising student from a country like Algeria to buy hardware for
1600 Eur is a joke.
And not all students are interested nor have the time to hook-up PIDE to
different front-ends to correctly use Isabelle.
1600 EUR was for my own high-end machine, and that is
ridiculously cheap for a professional working environment.
That example was to demonstrate that you don't have to invest 6000 EUR
for an iMacPro to get the same category of Engineering Workstation.
This thread was mainly about proper display technology: you can get that
easily for 350 EUR (graphics card + monitor).
Overall you probably need 800-1000 EUR for hardware to do serious
Isabelle applications.
We also need to be realistic that Formal Mathematics is a luxory of
well-educated people (not necessarily rich) -- uneducated people don't
know about the importance to invest in proper equipment.
Makarius
Email Gateway (Aug 22 2022 at 19:36):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I’m using a one-year old ThinkPad with a non-UHD display. My external
monitor, which I use most of the time, is quite a bit older and has a
resolution of 1280 × 1024 pixels. Some people just don’t have the
resources to buy lots of new and fancy stuff.
Nevertheless, I’ve been using Isabelle successfully for formal
mathematics way beyond basic examples. It’s just that the fonts have
always been looking a bit crappy with Isabelle 2017 and 2018, but after
a bit of tweaking I could live with the result. Other applications
(typically based on GTK+/Cairo) are yielding much better results on my
“vintage monitor”. I hope I’ll be able to make my decision when to buy a
new monitor independently of my expected future switch to Isabelle 2019.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:36):From: Makarius <makarius@sketis.net>
This thread is not about new and fancy stuff, but solid working
materials for everyday use.
I will not re-iterate this further, and merely ask people who disagree
to do some basic calculations about long-term investment into proper tools.
And anybody who insists in old stuff can just follow the Isabelle/jEdit
manual https://isabelle.in.tum.de/repos/isabelle/rev/b718a64d0d09
Makarius
Last updated: Apr 26 2024 at 04:17 UTC
