Zulip Chat Archive

Stream: Zulip meta

Topic: font issue on Android


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 01 2021 at 13:54):

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

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 13:57):

What version of Android / flavor of phone?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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