Zulip Chat Archive
Stream: general
Topic: changing doc-gen font
Eric Rodriguez (Jan 27 2022 at 17:41):
as we can see in docs#number_field.ring_of_integers_algebra, the issue with weird alignment has also now extended to doc-gen. The way to fix this in the infoview is by using a font like "dejavu sans mono"; however, this is not on Google Fonts, which the current docgen uses for webfonts (and is likely much faster than locally, because of caching). So I thought i'd look for other options - what font do you all use for the infoview that avoids this issue?
Eric Rodriguez (Jan 27 2022 at 17:42):
image.png whilst talking about this, I realised like all fun issues, it's machine dependent (this does not seem to happen on OS X) so here's a screenshot of the issue for those lucky to not have it [Windows 10, Firefox]
Oliver Nash (Jan 27 2022 at 17:43):
image.png
Fine on Firefox+MacOS FWIW.
Gabriel Ebner (Jan 27 2022 at 17:44):
Also fine on chromium+linux.
Eric Rodriguez (Jan 27 2022 at 17:44):
fine on Chrome/Windows, so seems to be a Firefox issue... drats
Gabriel Ebner (Jan 27 2022 at 17:44):
Although my 𝓞 looks very different from yours.
Gabriel Ebner (Jan 27 2022 at 17:45):
Also fine on firefox+linux.
Bhavik Mehta (Jan 27 2022 at 17:46):
Fine on Chrome/MacOS
Yaël Dillies (Jan 27 2022 at 17:46):
And Chrome+Windows
Gabriel Ebner (Jan 27 2022 at 17:47):
I think part of the issue is that 𝓞 is not included in Source Code Pro, so it renders differently for every one of us. (Here it is apparently picked up from FreeSerif???) If you find a fallback font containing 𝓞 that works fine, we can add it to doc-gen.
Gabriel Ebner (Jan 27 2022 at 17:47):
BTW, I don't think DejaVu Sans Mono contains that glyph either.
Eric Rodriguez (Jan 27 2022 at 17:54):
the rendered font on OSX Firefox seems to be one of the STIX fonts, which seem explicitly designed for mathematics and are on Google fonts - should I prepare a PR using this?
Eric Rodriguez (Jan 27 2022 at 18:54):
aaah it turns out the google fonts version does not include the 𝓞 character; I really don't want to include a whole file for this directly because of caching but I can't think of a better option currently
Gabriel Ebner (Jan 27 2022 at 18:57):
There's no caching advantage to using google's copy. Browsers disabled that sidechannel leak a long time ago.
Eric Rodriguez (Jan 28 2022 at 00:36):
finally sorted this - https://github.com/leanprover-community/doc-gen/pull/153
Eric Rodriguez (Jan 28 2022 at 00:36):
if someone can tell me what the correct thing to do with licenses is, would be much appreciated
Last updated: Dec 20 2023 at 11:08 UTC