font issue on Android

Stream: Zulip meta

[Kevin Buzzard]

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]

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

[Ryan Lahfa]

What version of Android / flavor of phone?

[Gabriel Ebner]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Ryan Lahfa]

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]

(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!)