search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
169 stars 27 forks source link

Weird font in infoview #192

Open abentkamp opened 7 months ago

abentkamp commented 7 months ago

From Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/A.20set.20that.20must.20be.20a.20singletoneral.20times.2E

updated Link: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20A.20set.20that.20must.20be.20a.20singleton

This user has a weird font issue in the infoview: image

Maybe this happens when the font "Source Code Pro" is not installed? This might be the user's default monospace font? We should probably ship the font with the website to make sure it's displayed correctly.

TentativeConvert commented 7 months ago

This should be part of the wider work package “Clean up css”. I don't think fonts are specified consistently, unless someone has recently worked on this. As for the choice of font, there's a long discussion on Zulip about fonts with sufficient unicode coverage, which seems to have temporarily settled on Henrik Böving's choice of the following fonts on the community doc pages:

code font: JuliaMono non-code font: Lato Medium

However, later in the same discussion, Henrik Böving does throw in Source Code Pro as an alternative:

Rustdoc uses: Source Code Pro for code Source Serif 4 for prose Fira Sans in a bunch of special locations like headlines etc.

So sticking with this font should also be fine as long as it's applied consistently and shipped with the website.

TentativeConvert commented 5 months ago

Another user has the same font issue on Safari on an iPad Pro.

joneugster commented 3 months ago

Hopefully, all code should now be JuliaMono and all non-code Roboto and both fonts are shipped with the page content if the user does not have them installed.