## 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:

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

Last updated: May 08 2021 at 21:09 UTC