Loogle: font

Stream: general

[Stuart Presnell]

Could the font on loogle.lean-lang.org be changed so that I and l look more distinct?

[Martin Dvořák]

Speaking of font, I recommend this one: https://www.jetbrains.com/lp/mono/

[Joachim Breitner]

Any suggestion for a good font? The docs page uses Source Code Prop. That would require switching to a mono-font, though.

[Notification Bot]

3 messages were moved here from #general > Loogle is live! by Joachim Breitner.

[Joachim Breitner]

Probably using the same as the doc page is the most reasonable choice that also side-steps possible bikeshedding :-)

[Martin Dvořák]

My suggestion is to use JetBrains Mono in all Lean tools.

[Joachim Breitner]

I’ll promise to change loogle when the doc page changes, so you only have one hill to fight on :-)

[Richard Copley]

I'll just mention that JuliaMono has better unicode coverage.

gif

fonts.gif

[Joachim Breitner]

@Stuart Presnell , https://loogle.lean-lang.org/ now uses Source Code Pro for the type (but not the theorem name). I’m not sure it’s prettier, but probably more legible. Does that work for you?

[Thomas Murrills]

Here's a website that's useful for comparing unicode support, by the way (which is mentioned on the Julia Mono page), and also links to some other useful font comparators

[Thomas Murrills]

The only thing I miss in Julia Mono are the nice ligatures of e.g. Fira Code or JetBrains...it has a few, but far fewer! (Fira Code and JetBrains also take pains to make alignment and whitespace nice via subtle ligatures for e.g. :=.)

[loki der quaeler]

perhaps https://monaspace.githubnext.com/

[Joachim Breitner]

Fancy stuff

[Henrik Böving]

Thomas Murrills said:

Here's a website that's useful for comparing unicode support, by the way (which is mentioned on the Julia Mono page), and also links to some other useful font comparators

I use Julia mono in all of my stuff so I would be very inclined to change the docs page to this if people like it better :D the only reason for the current font is that I copied it from the lean 3 variant

[Henrik Böving]

loki der quaeler said:

perhaps https://monaspace.githubnext.com/

I also saw this this morning, I was planning into checking if they support all of my Unicode needs. Although I am indecisive as to which of the 5 variants I like. I'm currently stick between neon and krypton

[Joachim Breitner]

I would be very inclined to change the docs page to this if people like it better :D

If you like it better, just do it, and see if people complain :-)

[Shreyas Srinivas]

Risky move. It could annoy too many people. Providing an option might avoid trouble

[Joachim Breitner]

If it annoys too many people, you can easily revert. I doubt it will, though.

[Joachim Breitner]

Providing options is often the worst option. It just increases complexity, adds distraction, and disappoints those who expect good defaults. Avoid options if possible :)

[Henrik Böving]

Shreyas Srinivas said:

Risky move. It could annoy too many people. Providing an option might avoid trouble

i have a feeling 90% of people wouldn't even notice at all or after a week

[Henrik Böving]

Oh and if you really despise a font you can always just inject custom CSS to overwrite it of course.

[Eric Wieser]

It would be cool if we could have the vscode extension offer a pop up to make the same font change; there's value in having the same font in the editor and documentation

[Shreyas Srinivas]

We can. It is not too much effort.

[Shreyas Srinivas]

You don't necessarily want the same font in different environments.

[Shreyas Srinivas]

About adding a recommendation: For one thing it isn't clear whether the mathlib docs are planned for vscode viewing

[Shreyas Srinivas]

I asked Marc a few days ago and haven't heard back.

[Shreyas Srinivas]

The other thing is if we do offer mathlib4 docs inside vscode, and if a webview is used which just loads the webpage, then we don't need to do anything. In the main editor area, it is possible to offer recommended settings, but nothing stops this being overridden.

[Shreyas Srinivas]

For the how, see : https://code.visualstudio.com/docs/getstarted/settings#_language-specific-editor-settings

[Eric Wieser]

Shreyas Srinivas said:

About adding a recommendation: For one thing it isn't clear whether the mathlib docs are planned for vscode viewing

I never intended to suggest reading the docs from within vscode; the recommendation I was suggesting was to switch the font for lean code. I just think it's helpful if the symbols in notation look the same between editor and docs

[Martin Dvořák]

loki der quaeler said:

perhaps https://monaspace.githubnext.com/

Texture healing is a complete new concept to me. My first impression is positive, but I don't know how ergonomic it will feel once I start staring at the text for 8 hours a day.

[Eric Wieser]

How's the unicode coverage?

[Joachim Breitner]

As someone who finds monospace typographically very unaesthetic, to the point that I use proportional fonts with manually crafted indentation in my papers (using the package polytable that's used by lhs2tex), I find the prospect of texture healing intriguing.

[Henrik Böving]

Eric Wieser said:

How's the unicode coverage?

I'll investigate this today!

[Henrik Böving]

Neon failure with unicode:
image.png
Argon failure:
image.png
(I'll leave out xenon and radon as they seem to be geared more towards prose writing)
krypton failure:
image.png

and this is just from a brief scroll through the abbreviations.json until I found something that looks weird, there is probably more that i didnt catch first sight

in JuliaMono all of these stay at least within the quotation marks. I also find basic things to be more distinguished in JuliaMono, for example or vs v (or is on top):
image.png

and we have things like this in neon:

image.png

so I'm probably gonna look into maybe changing the monospace font to JuliaMono and see how it looks later today.

[eyelash]

Since JetBrains Mono Source Code Pro is an open source project, if the only problem with that font is the Unicode coverage, you could also open a bug report with them and see if they're interested in fixing the coverage.

[eyelash]

The same is also true for JetBrains Mono and probably other fonts mentioned in this thread. In general I feel it would be a good idea to open bug reports for these fonts so that the coverage can be improved and Lean users have more fonts available that work well with Lean.

[Julian Berman]

There's https://github.com/adobe-fonts/source-code-pro/issues/49 and https://github.com/JetBrains/JetBrainsMono/issues/561 it seems for the two of those respectively already.

[Henrik Böving]

I mean both of those have been open for a while and are still not finished yet so I'm not going to hold my breath on that.

I have a local change that does two things now:

1. Change the code font to JuliaMono
2. Change the non code font to Lato Medium, this is the same font that the Julia docs use for their non code stuff so I decided to give it a go as well.

My subjective perception is: The JuliaMono one definitely looks better but that is probably because I use it myself. I do like the more ...minimalist? Way that Lato Medium looks although I am not yet fully sold on it.

Either way I'll now just push the changes and given the fact that initially everyone does of course dislike change I'll leave it be there for a week or something like that. If complaints die down by then I'll leave it be and otherwise we can always revert one or both back.

[Joachim Breitner]

I like the commit message :-D

[Joachim Breitner]

Loogle is following suite

[Yaël Dillies]

@Henrik Böving, while we're at it, could we revert the font in the search results to be the one we had in docs3# ? The monospacing is unnecessary there and having a non-monospace font makes you read a (significantly) greater portion of each name.
mathlib
mathlib4

[Yaël Dillies]

This has been bothering me for several months.

[Joachim Breitner]

Is Julia a wider font than Source Pro? My eyes seem to desire something more condensed.

[Henrik Böving]

Yaël Dillies said:

This has been bothering me for several months.

Yes I can do that let me figure out the CSS incarnation

[Henrik Böving]

Joachim Breitner said:

Is Julia a wider font than Source Pro? My eyes seem to desire something more condensed.

Hm, I don't really know.

[Joachim Breitner]

Anyways, as you say, let’s use it for a week before jumping to conclusions :-)

[Joachim Breitner]

Although would it be heretic to consider a non-monospace font for docs and loogle? There is no vertical alignment that would call for one, and I find proportional fonts to be more readable, if only because they take less space. (A good unicode coverage and distinctive letters are of course still the primary goal.)

[Yaël Dillies]

I think it's useful-ish to distinguish code from docstrings, but actually the code font needn't be monospace for that purpose.

[Joachim Breitner]

paper.png
This is from a paper of mine, where I tried to choose a proportional font for the code that looks just distinct enough from the main body to be recognizable, and has distinct l and I. In this case the font is Ubuntu, but of course for a paper on Haskell I don’t need particularly high Unicode coverage (none actually beyond ASCII), so this is not a concrete recommendation.

[Henrik Böving]

I don't really like that view personally but if we find something that enough of the interested people can agree on and it has enough unicode sure.

To throw yet another data point in. Rustdoc uses:

1. Source Code Pro for Code
2. Source Serif 4 for prose
3. Fira Sans in a bunch of special locations like headlines etc.

[Henrik Böving]

@Yaël Dillies
image.png
yay or nay?

[Yaël Dillies]

Oooh, yeah this is quite good.

[Yaël Dillies]

although I would expect the search box to have the same font as the results

[Henrik Böving]

Yaël Dillies said:

although I would expect the search box to have the same font as the results

Hmmm, that is supposed to be the same font according to my CSS... let's see

[Eric Wieser]

@Joachim Breitner, I thought that opinion on proportional fonts for code died with the final release of the Plan 9 OS and its acme editor!

[Henrik Böving]

No I can't figure this one out, maybe a CSS wizard here can tell me whats up: According to my CSS style it should be using Lato Medium for the thing in the box but:
image.png
it obviously isn't (the text below is Lato Medium, the most clear difference is at the J)

[Joachim Breitner]

I thought that opinion on proportional fonts for code died with the final release of the Plan 9 OS and its acme editor!

There is a German saying, “Totgesagte leben länger”.

But it’s probably telling that only my single-author papers use that style :-D

[Joachim Breitner]

@Henrik Böving , might be this: https://stackoverflow.com/a/6080482/946226

[Henrik Böving]

Aha that's indeed it, why would you make these semantics consistent anyways mhm..

[Schrodinger ZHU Yifan]

There is another font https://commitmono.com/ designed for cleaness.

[Trebor Huang]

Agda papers often use proportional fonts too with automatically generated alignments. See the docs for how they did it. But do we really need than much alignment except at the left boundary?

[Eric Wieser]

Can you link to the docs you're thinking of?

[Trebor Huang]

https://agda.readthedocs.io/en/v2.6.4/tools/generating-latex.html#alignment

[Eric Wieser]

Thanks! I thought you were describing in-editor support, but I see it's only about LaTeX output. Is there an example pdf anywhere?

[Trebor Huang]

For example https://arxiv.org/abs/2001.11001

[Trebor Huang]

I have also typeset stuff with the same package https://arxiv.org/pdf/2310.02051.pdf
The grey part and green parts use proportional font with no alignment except on the left

[Trebor Huang]

I think they still look pretty decent

[Eric Rodriguez]

On the font conversation, the font for the playground is bad too:

image.png