Zulip Chat Archive

Stream: general

Topic: font choice, lean, terminal

Bernd Losert (Dec 06 2021 at 16:39):

I'm working with lean from the terminal. I'm noticing that some of the fancier math symbols are not rendered. For example, the 𝓟 used for principal ultrafilters is rendered as � for me in the terminal, regardless of the font that I use. I'm currenty using unifont, which should have all these crazy symbols.

Is there a monospaced terminal font that covers all the symbols in lean/mathlib or do I have to use a terminal/IDE with a fallback font like stix?

Johan Commelin (Dec 06 2021 at 16:46):

cc @Julian Berman ?

Gabriel Ebner (Dec 06 2021 at 16:52):

The recommendation I've put into the vscode-lean readme years ago is to use Source Code Pro Medium with DejaVu Sans Mono as fallback. On Linux it should be enough to install both and set Source Code Pro as the font in your terminal.

Gabriel Ebner (Dec 06 2021 at 16:54):

I'm also using Fira Mono, which works as well.

Julian Berman (Dec 06 2021 at 16:56):

I use Inconsolata (the one true best monospace font, come fight me) and it seems fine rendering that 𝓟 and any other symbols I've used/encountered from mathlib (I use kitty as my terminal which does support configuring fallback fonts should they be needed but I've left them at the default which on macOS probably means it's using Monaco or Courier as a fallback)

Julian Berman (Dec 06 2021 at 16:56):

But I trust Gabriel's (and vscode-lean's) recommendations as well of course

Bernd Losert (Dec 06 2021 at 16:57):

I'm using Terminal.app on Mac OS.

Julian Berman (Dec 06 2021 at 16:58):

Ah, yeah I mean I'd recommend other terminals on macOS for other reasons mainly, kitty is great, as is iTerm.app, but for this, let's see if it matters, I'll try Terminal.app for a minute

Bernd Losert (Dec 06 2021 at 16:59):

Well, I just tried DejaVu Sans Mono and it's the same result.

Julian Berman (Dec 06 2021 at 16:59):

I see the correct symbol with Inconsolata in Terminal.app

Bernd Losert (Dec 06 2021 at 17:01):

I tried Inconsolata just now too. Same result.

Bernd Losert (Dec 06 2021 at 17:01):

Weird.

Julian Berman (Dec 06 2021 at 17:01):

With DejaVu Sans Mono which I just installed, I see the correct symbol too

Julian Berman (Dec 06 2021 at 17:01):

So yeah something else is up.

Bernd Losert (Dec 06 2021 at 17:02):

Are you using macOS Monterey?

Gabriel Ebner (Dec 06 2021 at 17:02):

I've just checked and apparently on my machine FreeSerif is the fallback for that character..

Julian Berman (Dec 06 2021 at 17:03):

How did you check that, I was just looking for how to do so on macOS (I doubt it's the same way, but yeah just curious?)

Julian Berman (Dec 06 2021 at 17:03):

Bernd Losert said:

Are you using macOS Monterey?

yes

What's your $LANG $LC_ALL and $TERM perhaps

Gabriel Ebner (Dec 06 2021 at 17:04):

How did you check that, I was just looking for how to do so on macOS (I doubt it's the same way, but yeah just curious?)

I'm not sure if there is a better way, but this gives you some information:
env FC_DEBUG=4 pango-view -t '𝓟' </dev/null | grep family

Gabriel Ebner (Dec 06 2021 at 17:05):

You can also go into the developer tools of your favorite browser, that also shows which fonts were used for rendering.

Bernd Losert (Dec 06 2021 at 17:07):

TERM is xterm-256color, LANG and en_US.UTF-8 are en_US.UTF-8

Julian Berman (Dec 06 2021 at 17:11):

OK that seems fine. I'm installing what's needed to run Gabriel's command, and I just tried on a terminal without all my shell config and can still see that character fine, so not sure yet what's up.

Bernd Losert (Dec 06 2021 at 17:18):

Aha! I discovered the problem: It does not work inside GNU screen. Outside of GNU screen, I have no problems.

Johan Commelin (Dec 06 2021 at 17:19):

How about tmux?

Julian Berman (Dec 06 2021 at 17:19):

aha! OK, sorry, should have asked that.

Johan Commelin (Dec 06 2021 at 17:19):

It's supposed to be the better GNU screen

Julian Berman (Dec 06 2021 at 17:19):

I'm inside tmux, and it works, but yeah that'll depend on your $TERM

Bernd Losert (Dec 06 2021 at 17:20):

Thanks for helping guys. I guess I'll have to work outside of screen for now until I figure out the issue.

Julian Berman (Dec 06 2021 at 17:20):

in fact inside screen it should work too, but your $TERM shouldn't be xterm-256color in there, was that what you get?

Julian Berman (Dec 06 2021 at 17:20):

you should get something like screen-256color

Bernd Losert (Dec 06 2021 at 17:20):

Yeah, inside screen, TERM is screen-256color.

Julian Berman (Dec 06 2021 at 17:22):

(FWIW following Gabriel's browser advice I see the font used for me is STIXGeneral, which looks like some generic fallback shipped with macOS for science-y symbols, so I assume you should have no issues there, it's just an OS font you'll have)