In the last line of the "goals" output, _ are not visible

[RalfJung]

Consider this code for example:

Lemma my_lemma : True. Proof. exact I. Qed.
About my_lemma.

This produces output as follows on my system:

As you can see, in the last line the _ are not visible, and look like spaces.

Strangely, when I copy-paste that text it does contain the underscore. My guess is that the bottom few pixels of the output are truncated, cutting of the underscores.

[RalfJung]

I have setup my system to use "Fira Code" as my monospace font, and I think that is what vscodium uses.

[Durbatuluk1701]

It produces the following for me using 'JetBrainsMono Nerd Font Mono' and the underscores are present:

I also tested with Consolas, 'Courier New', and monospace and they all seem to display underscores, which sort of leads me to believe it must be related to Fira Code. Will test with it next.

[RalfJung]

Fira Code has the underscores really low, as you can see in my screenhot. That's probably why it is more susceptible to being cut off at the bottom, if just last last pixel or two of the line are missing.

[Durbatuluk1701]

I installed Fira Code and tried it in VsCode v1.93.0 (on Windows via WSL) and got this:

Are you using vscodium and/or not windows? Might be related to one of those if so

[RalfJung]

This is vscodium on Linux.

I checked the font settings and they are set to 'Droid Sans Mono', 'monospace', monospace. If I set it to Noto Sans Mono, the underscores become visible. It's a bit hard to figure out which font names I can even use there, not all the fonts on my system work and vscode doesn't seem to have a way to list the fonts so that I can just select one...

[Durbatuluk1701]

I have been able to reproduce this with monospace on Linux and vscode, but the exact same setup on Windows with font monospace does not cause the issue.

[RalfJung]

monospace will be whatever your system default monospace font is.

[Durbatuluk1701]

I think I have tracked down the offending font: DejaVu Sans Mono

I can confirm that with this font the underscores are not displayed in Linux, but even with DejaVu Sans Mono they are displayed in Windows

[RalfJung]

Ah you are right, Fira Mono is actually fine -- I had some other trouble with my setup that meant some of my fonts were not picked up.