Zulip Chat Archive

Stream: Zulip meta

Topic: font issue on Android


Kevin Buzzard (Feb 01 2021 at 13:50):

On my mobile, with the Zulip desktop app, this code:

import tactic

example {A} (Q : Prop) (P P₀ : A  Prop) (h : Q   a : A, P₀ a) (q : Q)
  (H :  a : A, P₀ a  P a) : ( a : A, P a) :=
begin
  rcases h q with a, h⟩,
  refine a, _⟩,
  exact H _ h,
end

looks like this:

Screenshot_20210201-134748.png

One thing I find particularly surprising about this is that of the two symbols, the first is displayed as a box and the second is not. Is it possible to fix this issue somehow? I often find myself struggling to read pasted Lean code using the Android Zulip app on my phone.

Eric Wieser (Feb 01 2021 at 13:54):

Perhaps better targeted at #Zulip meta? This has got me in the past too though.

Ryan Lahfa (Feb 01 2021 at 13:57):

What version of Android / flavor of phone?

Gabriel Ebner (Feb 01 2021 at 13:57):

This doesn't help you, but I can see the characters just fine on Android 10 with Firefox. I think this can theoretically be fixed by the zulip developers, they'd just need to add a fallback font.

Kevin Buzzard (Feb 01 2021 at 14:03):

Moto g^7 play with Android 10 but I assume I'm not the only person with this problem. Zulip app v27.157 (according to settings -> diagnostics). Is the issue with the app or with my font set? I can't figure out how to move this to the Zulip meta stream.

Eric Wieser (Feb 01 2021 at 14:04):

Same issue on android 11 - but i see the issue in github emails in the Gmail app, so I think this is a system-wide problem

Kevin Buzzard (Feb 01 2021 at 14:06):

Using duckduckgo browser on the same phone I see boxes in exactly the same places as the app screenshot.

Kevin Buzzard (Feb 04 2021 at 10:49):

In Android settings -> System->Developer options there is an option to change "Headline/body font" (I have "Device default", "Raleway" and "Noto Serif/Source Sans Pro") but these options do not seem to change the font in the Zulip app.

Julian Berman (Feb 04 2021 at 14:03):

If it's the same in your browser it seems unlikely to be related to zulip specifically, it's yeah some global font that's missing glyphs

Julian Berman (Feb 04 2021 at 14:03):

I didn't read it carefully but maybe https://github.com/zulip/zulip-mobile/issues/3885 is also your issue -- or if not maybe posting an issue nevertheless on zulip-mobile is a sneaky way to ask where they think you need to twiddle

Julian Berman (Feb 04 2021 at 14:05):

hm no reading slightly more carefully the solution there won't help you since it looks like it's something the zulip app needs to do

Julian Berman (Feb 04 2021 at 14:05):

if your device is rooted I think you can put a fallback font yourself somewhere in /etc if I remember right

Ryan Lahfa (Feb 04 2021 at 18:14):

Julian Berman said:

if your device is rooted I think you can put a fallback font yourself somewhere in /etc if I remember right

If you're rooted, and, you use something like https://github.com/topjohnwu/Magisk

You can install plugins/modules to add more fonts easily from the Magisk application

Eric Wieser (Dec 15 2023 at 14:07):

(since this thread was linked to from elsewhere, the tracking bug for this is https://bugs.chromium.org/p/chromium/issues/detail?id=764754; please +1 it!)


Last updated: Dec 20 2023 at 11:08 UTC