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):

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