Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 10/02/2019 20:08, Peter Lammich wrote: > No luck on my machine. The font rendering still looks slightly > blurred. > > However, I'm using an old Linux (Ubuntu 16.04) ... may that be the > reason? I don't think so, but you can make a quick test by booting current Ubuntu 18.04 from an USB stick. The graphics drivers could make a difference. Note that the jdk-11 distribution includes a copy of libfreetype.so, so it appears to be reasonably self-contained in that respect. (I did not read the relevant sources, because it is split between a Java and a native part in C, and the latter sources always require extra work to locate.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
No luck on my machine. The font rendering still looks slightly blurred. However, I'm using an old Linux (Ubuntu 16.04) ... may that be the reason? -- Peter On So, 2019-02-10 at 20:01 +0100, Christian Sternagel wrote: > This is just to confirm that the result looks really great on my > linux > (Fedora 29 with i3) setup. Thanks! > > chris > > On 2/10/19 7:47 PM, Makarius wrote: > > > > On 08/02/2019 10:03, Christian Sternagel wrote: > > > > > > > > > I am glad to hear that others have the same experience, I thought > > > my > > > eyes were going bad ;) > > > > > > But seriously, "buy a new screen" is not always possible. For > > > example, > > > in the upcoming summer term I am teaching an Isabelle class at > > > the > > > University of Innsbruck. In my experience (and I just reconfirmed > > > this > > > for the room I will be teaching in), the projectors we have here > > > a > > > typically rather old (and have low resolution, but that is a > > > different > > > story). > > > > > > At the moment there is a palpable difference (font rendering > > > crispness > > > wise) between using Isabelle2018 with projector (which I will do > > > anyway > > > for my class) and some recent development version (sorry I didn't > > > note > > > down what changeset I used for testing my setup). > > Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK) > > are > > different in many ways, and it is definitely required to get used > > to the > > new look of font rendering. (For me Isabelle2018 already looks very > > strange.) > > > > With proper parameters -- in software and hardware -- fonts should > > come > > out better than before. > > > > > > First of all, sub-pixel rendering should be enabled, see this NEWS > > entry > > from Isabelle/f714114b0571 (25-Oct-2018): > > > > *** Isabelle/jEdit Prover IDE *** > > > > * Improved sub-pixel font rendering (especially on Linux), thanks > > to > > OpenJDK 11. > > > > (In Java 8, sub-pixel rendering made things worse.) > > > > Since that that NEWS entry is a bit too implicit, I have now > > changed the > > default to enable "Subpixel HRGB" always on all platforms > > (Isabelle/f610115ca3d0). I have checked my usual test machines for > > Windows and macOS, to see that it all looks fine. > > > > > > Secondly, I have done some more research on FreeType, the renderer > > used > > for OpenJDK on Linux. It appears that the DejaVu family gets some > > special treatment if it shows up under its original name, but not > > if it > > is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts > > in > > Isabelle/4791988fcbc4 to impose the FreeType auto-hinting > > beforehand to > > the TrueType file: this leads to isabelle_fonts-20190210 in > > Isabelle/7e5a7a11d5d1. > > > > > > In summary: > > > > * Isabelle font rendering should be once again slightly better on > > Linux. > > > > * There is a small risk that it has slightly degraded on Windows > > and > > macOS. > > > > In other words: early adopters should look closely if it is all > > fine. We > > are (very slowly) moving towards the Isabelle2019 release > > (presumably > > June 2019), and everything needs to be beyond doubt when released. > > > > > > Makarius > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel > le-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
This is just to confirm that the result looks really great on my linux (Fedora 29 with i3) setup. Thanks! chris On 2/10/19 7:47 PM, Makarius wrote: > On 08/02/2019 10:03, Christian Sternagel wrote: >> >> I am glad to hear that others have the same experience, I thought my >> eyes were going bad ;) >> >> But seriously, "buy a new screen" is not always possible. For example, >> in the upcoming summer term I am teaching an Isabelle class at the >> University of Innsbruck. In my experience (and I just reconfirmed this >> for the room I will be teaching in), the projectors we have here a >> typically rather old (and have low resolution, but that is a different >> story). >> >> At the moment there is a palpable difference (font rendering crispness >> wise) between using Isabelle2018 with projector (which I will do anyway >> for my class) and some recent development version (sorry I didn't note >> down what changeset I used for testing my setup). > > Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK) are > different in many ways, and it is definitely required to get used to the > new look of font rendering. (For me Isabelle2018 already looks very > strange.) > > With proper parameters -- in software and hardware -- fonts should come > out better than before. > > > First of all, sub-pixel rendering should be enabled, see this NEWS entry > from Isabelle/f714114b0571 (25-Oct-2018): > > *** Isabelle/jEdit Prover IDE *** > > * Improved sub-pixel font rendering (especially on Linux), thanks to > OpenJDK 11. > > (In Java 8, sub-pixel rendering made things worse.) > > Since that that NEWS entry is a bit too implicit, I have now changed the > default to enable "Subpixel HRGB" always on all platforms > (Isabelle/f610115ca3d0). I have checked my usual test machines for > Windows and macOS, to see that it all looks fine. > > > Secondly, I have done some more research on FreeType, the renderer used > for OpenJDK on Linux. It appears that the DejaVu family gets some > special treatment if it shows up under its original name, but not if it > is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts in > Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to > the TrueType file: this leads to isabelle_fonts-20190210 in > Isabelle/7e5a7a11d5d1. > > > In summary: > > * Isabelle font rendering should be once again slightly better on Linux. > > * There is a small risk that it has slightly degraded on Windows and > macOS. > > In other words: early adopters should look closely if it is all fine. We > are (very slowly) moving towards the Isabelle2019 release (presumably > June 2019), and everything needs to be beyond doubt when released. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 05/02/2019 20:19, Makarius wrote: > On 05.02.19 11:43, Peter Lammich wrote: >> >> Is this worsening due to another Java version, due to the new Isabelle >> font, or has it some other reasons? How to find out? > > From a distance, I would say that this is a matter of the Java 11 > font-renderer, which is provided by https://adoptopenjdk.net. The one by > Oracle is much worse -- OpenJdk not the non-free Java. (Note that the > license change of non-free Oracle Java no longer allows to bundle it.) Even more, JDK 11 from Oracle is now distributed as non-free: users have to pay a subscription to use it in applications. Only some testing and development is allowed without extra payment. (See https://www.oracle.com/technetwork/java/javase/terms/license/javase-license.html). Java 8 is being phased out after Jan-2019. Since the Java community is notoriously slow in giving up legacy versions, there will be a bit more time to hold the breath and pretend that nothing has happened. In contrast, Isabelle is already on Java 11: it performs much better than Java 8, especially on high-end hardware with many cores (potentially also on "containers" like Docker). I have already seen some Isabelle/Scala scalability problems some months ago; luckily this has been resolved with Java 11. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 08/02/2019 10:03, Christian Sternagel wrote: > > I am glad to hear that others have the same experience, I thought my > eyes were going bad ;) > > But seriously, "buy a new screen" is not always possible. For example, > in the upcoming summer term I am teaching an Isabelle class at the > University of Innsbruck. In my experience (and I just reconfirmed this > for the room I will be teaching in), the projectors we have here a > typically rather old (and have low resolution, but that is a different > story). > > At the moment there is a palpable difference (font rendering crispness > wise) between using Isabelle2018 with projector (which I will do anyway > for my class) and some recent development version (sorry I didn't note > down what changeset I used for testing my setup). Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK) are different in many ways, and it is definitely required to get used to the new look of font rendering. (For me Isabelle2018 already looks very strange.) With proper parameters -- in software and hardware -- fonts should come out better than before. First of all, sub-pixel rendering should be enabled, see this NEWS entry from Isabelle/f714114b0571 (25-Oct-2018): *** Isabelle/jEdit Prover IDE *** * Improved sub-pixel font rendering (especially on Linux), thanks to OpenJDK 11. (In Java 8, sub-pixel rendering made things worse.) Since that that NEWS entry is a bit too implicit, I have now changed the default to enable "Subpixel HRGB" always on all platforms (Isabelle/f610115ca3d0). I have checked my usual test machines for Windows and macOS, to see that it all looks fine. Secondly, I have done some more research on FreeType, the renderer used for OpenJDK on Linux. It appears that the DejaVu family gets some special treatment if it shows up under its original name, but not if it is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts in Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to the TrueType file: this leads to isabelle_fonts-20190210 in Isabelle/7e5a7a11d5d1. In summary: * Isabelle font rendering should be once again slightly better on Linux. * There is a small risk that it has slightly degraded on Windows and macOS. In other words: early adopters should look closely if it is all fine. We are (very slowly) moving towards the Isabelle2019 release (presumably June 2019), and everything needs to be beyond doubt when released. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 04/02/2019 14:17, Makarius wrote: > On 04/02/2019 10:37, Lars Hupel wrote: >> Is this related to the latest Poly/ML changes? The "slow" job still runs >> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware >> is 8-core LRZ VM. > > I can confirm this: see > https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html > > I have switched back to stable polyml-5.7.1-8 for now (see > Isabelle/a5732629cc46) and will be unavailable for the next few days. This did not change the non-termination, but the following helps: changeset: 10116:9181c1974aa0 tag: tip user:wenzelm date:Sun Feb 10 16:49:10 2019 +0100 files: thys/Flyspeck-Tame/PlaneGraphIso.thy description: adapted to Isabelle/7e4966eaf781 -- avoid non-termination; changeset: 69777:7e4966eaf781 parent: 69767:d10fafeb93c0 user:haftmann date:Thu Jan 31 13:08:59 2019 + files: NEWS src/HOL/Analysis/Caratheodory.thy src/HOL/Analysis/Convex.thy src/HOL/Analysis/Elementary_Topology.thy src/HOL/Analysis/Embed_Measure.thy src/HOL/Analysis/Homotopy.thy src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Binomial.thy src/HOL/Complete_Lattices.thy src/HOL/Enum.thy src/HOL/Fun.thy src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Probability/ex/Dining_Cryptographers.thy src/HOL/Set.thy src/HOL/Set_Interval.thy src/HOL/UNITY/Comp/Alloc.thy description: proper congruence rule for image operator I have merely applied the recommendation from the NEWS: INCOMPATIBILITY; consider using declare image_cong_simp [cong del] in extreme situations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
