search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
332 stars 68 forks source link

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

Open RalfJung opened 3 weeks ago

RalfJung commented 3 weeks ago

Consider this code for example:

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

This produces output as follows on my system:

image

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 commented 3 weeks ago

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

Durbatuluk1701 commented 3 weeks ago

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

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 commented 3 weeks ago

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 commented 3 weeks ago

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

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

RalfJung commented 3 weeks ago

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 commented 3 weeks ago

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 commented 3 weeks ago

monospace will be whatever your system default monospace font is.

Durbatuluk1701 commented 3 weeks ago

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 commented 2 weeks ago

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.