Recommended font

Stream: general

[Ricardo Prado Cunha]

Is there a recommended font for Lean that distinguishes symbols that look alike? I've found myself getting confused between things like \perp and \bot or \|| and \parallel.

[Eric Wieser]

In VSCode, you can hover over a symbol to see both what it means and how to type it

[Eric Wieser]

For those ambiguous cases, usually it's obvious from the context (and the other symbol would be a syntax error)

[Ricardo Prado Cunha]

Yes, but I'd still prefer to be able to tell what a symbol is at -a-glance.

[Martin Dvořák]

I use JetBrains Mono. It is great for coding in general, but I have trouble distinguishing vν∨ from each other in this font.

[Shreyas Srinivas]

I think this comes up often. I recall bringing it up in my early lean days. There are many more ambiguous cases, with various dots, with the divisibility symbol etc. I don't immediately see how any fonts can help with those. Nevertheless there are intuitively obvious ASCII variants for some standard notations especially propositional stuff.

In general, it appears that lean caters to mathematicians' notational needs as far as possible, even at the expense of clarity. The trade-off is that lean's extension will do what Eric says. It currently mitigates some of the confusion that is caused by the use of very similar looking symbols with its tooltips and syntax errors. This still doesn't help when one is reading the docs and trying to use notation from there. For example when starting out, the divisibility notation stumped me for a while (it is actually \|). Unfortunately, mathematical notation was not devised with the anticipation that it would have to be typed into a text editor some day.

Maybe some day there will be a math specific font that renders unicode math like latex does. Or maybe there will be an additional rendering buffer in text editors that keeps track of which symbols are to be in text mode and which ones are to be in math mode, and then render everything in HTML with mathml where required: A more advanced version of markdown editors that render their text in-place.

[Eric Wieser]

There is an easy solution to using notation from the docs; copy and paste it, then ask the editor how to type it.

[Eric Wieser]

(of course if the docs could show it directly that would be great too, but that doesn't help people using custom or outdated editor config)

[Alex J. Best]

After the port I think it would be good to review how many of these weird notations are needed with lean 4. I'm not an expert in this but I'd hope that maybe we have more expressivity now to not have to pick different symbols in a situation where the end user wouldn't be confused. Divisibility is a good example of this, but also for instance the \[- strange brackets for commutators / lie theory.

[Shreyas Srinivas]

Some of those notations are common in mathematics right?

[Kevin Buzzard]

Yes, and we are happy to interpret what notation means from context (we sometimes even have the same letter representing two things and again just observe that it's clear which usage is intended)

[Martin Dvořák]

Shreyas Srinivas said:

I don't immediately see how any fonts can help with those.

I think it is worth giving it a try. Does anybody have a grant that could pay for a professional custom font designer?

My suggestion would be to fork JetBrains Mono and fix those few problematic characters. I believe that, if we all start using this optimized font, our productivity will increase.

[Henrik Böving]

Martin Dvořák said:

I use JetBrains Mono. It is great for coding in general, but I have trouble distinguishing vν∨ from each other in this font.

image.png

[Henrik Böving]

I spent a day or two trying out random monospace fonts once and I ended up with JuliaMono, has served me well so far^^

[Eric Wieser]

We should continue to be using ∣ (U+2223 DIVIDES) for divide, right? If in doubt we should pick the appropriate character not just the one that's easy to type (ASCII |)

[Mario Carneiro]

I think the main reason we aren't using ascii | is because it conflicts with various kinds of built in syntax

[Martin Dvořák]

My suggestion for a custom Lean font would be to drop the requirement of ∧∨ being in the same height. If they are in the same height, we end up having trouble either distinguishing ∧^ or distinguishing ∨v (most fonts I have seen had too much similarity in the latter).

[Alex J. Best]

In order to cause less confusion I'd rather there weren't similar but distinct characters cropping up in the source. So if a unicode character is too close to an ascii one like pipe, and can be avoided in Lean 4, I'd vote to switch to the simpler character even if it is the "wrong" one according to unicode (we really have a lot of symbols with the "wrong" meaning already so I don't see that as a regression)

[Eric Wieser]

I think most of the places where we use symbols with the wrong meaning are places where there is no right symbol available (or the right symbol exists but is already used in other syntax).

[Eric Wieser]

I made two changes in the last few months to change things towards the right symbol; the previous use of PARALLEL for norm was really annoying on some platforms as the font chose a slightly slanted symbol (which is fairly reasonable for parallel, but looks very silly when used on both sides of a norm)

[Eric Wieser]

It would be great if syntax errors that appear on a non-word character could include a "did you mean" which suggests "similar" unicode characters (and any information available about the notation)

[Martin Dvořák]

Alex J. Best said:

In order to cause less confusion I'd rather there weren't similar but distinct characters cropping up in the source.

Would you go as far as abandoning ∨ for or?

[Shreyas Srinivas]

I suspect if "latex" characters were rendered in bold font like some markdown editors do, this would alleviate a lot of problems

[Patrick Massot]

I wouldn't complain. Writing ∨ instead of or to save one character seems to be pure obfuscation.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Not only bold, but slightly larger font size. I have never had trouble with markdown inline math.

[Martin Dvořák]

Patrick Massot said:

I wouldn't complain. Writing ∨ instead of or to save one character seems to be pure obfuscation.

Assuming you replace ∨ by or but nothing else changes, it would be weird to have Or as a prefix operator and or as an infix operator.

[Martin Dvořák]

The comment above is about Lean 4. In Lean 3 or was the prefix operator, which I used sometimes.

[Martin Dvořák]

My point is that, for the sake of readability, we should keep infix operators written in non-letter characters.

[Kyle Miller]

It seems unlikely to me that disjunctions will ever be anything other than ∨, but Lean for sake of readability does give syntax highlighting:

image.png

Python's or and and operators are readable to people who use Python, so I feel like we need a Wikipedia-style "[whose?]" tag on that "for sake of readability" :wink:

One could also argue that having Or be the type itself and or be the operator has nicer parallelism than Or and ∨.

[Martin Dvořák]

Parentheses work differently in Python. You wouldn't encounter

foo bar or foo baz

in Python, but we want to write

foo bar ∨ foo baz

in Lean.

Therefore, we deal with infix operators differently than Pythoners.
My point is that ∨ instead of or is not "to save one character" but to make the operator clearly non-alphanumeric.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

How feasible is it to change the way specific characters are rendered within the extension? That is, maintain a table of symbols that are math. If found, render the character with a slightly different font style.

[Shreyas Srinivas]

EDIT: the zulip android app seems to be double sending my messages while showing me a loading bar.

[Julian Berman]

so I feel like we need a Wikipedia-style "[whose?]" tag on that "for sake of readability

https://www.vidarholen.net/~vidar/An_Empirical_Investigation_into_Programming_Language_Syntax.pdf FWIW is a nice paper which investigated some similar things, albeit for boolean or they did not compare ∨ which wasn't part of the alternatives there.

The two groups were "programmers" and "non-programmers", and in particular not "mathematicians" of course, and also the paper is old, but it's cute at least to skim I think still, even if the results are probably not useful to answer this question (though hey maybe folks here who have undergraduate math students can torture them into repeating the experiment).

[Eric Rodriguez]

On the terms of fonts, I think the still recommended one for most cases is "DejaVu Sans Mono", especially in the infoview

[Eric Rodriguez]

It doesn't have the clarity with all symbols but it is properly monospaced for the vast majority of them

[Eric Rodriguez]

I'm not sure if it's still an issue in Lean4, but due to how the widgets are drawn in Lean3, the lack of monospacing on some more rare characters can really cause ugly looking tactic states

[Eric Rodriguez]

stuff like this:
image.png

[Eric Wieser]

Eric Rodriguez said:

On the terms of fonts, I think the still recommended one for most cases is "DejaVu Sans Mono", especially in the infoview

This one also has the advantage of being easy to use in LaTeX

[Martin Dvořák]

Henrik Böving said:

I spent a day or two trying out random monospace fonts once and I ended up with JuliaMono, has served me well so far^^

I just tried their demo. My ability to distinguish between ∨ and v in JuliaMono is even worse than in other fonts.

[Martin Dvořák]

Eric Rodriguez said:

On the terms of fonts, I think the still recommended one for most cases is "DejaVu Sans Mono", especially in the infoview

Their demo does not show me ∨ at all. Can you please send a screenshot snippet with ∨v in DejaVu Sans Mono?

[Henrik Böving]

It's possible that Eric's editor is going for a fallback font if DejaVu Sans Mono doesn't have it, that's one of the main things I avoided with Julia because they actually have lots of unicdoe characters monospaced while lots of other fonts do fallbacks to non monospace stuff

[Eric Wieser]

I think usually what happens is the font is just missing the characters altogether, and then the OS/application picks another font to fallback to

[Martin Dvořák]

Kyle Miller said:

It seems unlikely to me that disjunctions will ever be anything other than ∨

I like ∨ for disjunctions. I had been heavily using ∨ and ∧ in pen-and-paper MathematiCS before I stumbled across Lean (even before Lean was created). However, the visual similarity between ∨ and v on computer screen drives me crazy. As for ν (i.e., \nu), I don't care; I already decided that I will never use that character.

[Mac Malone]

@Martin Dvořák You could always just use the ASCII art for disjunction and conjunction (i.e., \/ and /\).

[Mac Malone]

Which, if a font supports ligatures, can look quite good (and clearly distinct from v or V due to their width).

[Martin Dvořák]

Mac said:

Martin Dvořák You could always just use the ASCII art for disjunction and conjunction (i.e., \/ and /\).

For \/ and /\ to make sense, we all would have to switch to it, which won't happen.

[Shreyas Srinivas]

Martin Dvořák said:

Mac said:

Martin Dvořák You could always just use the ASCII art for disjunction and conjunction (i.e., \/ and /\).

For \/ and /\ to make sense, we all would have to switch to it, which won't happen.

It is annoying to type these in Coq, and gives em a headache when reading it. Typing is annoying because when typing fast it is very easy to mix up the order of / and \ and then you spend some time wondering where it all went wrong.
(I know coq has some editor support for unicode, but it is very patchy as far as coq-lsp goes).

[Martin Dvořák]

My position on this is still the same. I want to change font. I don't want to change Lean.

[Arthur Paulino]

A trick that I did was to install some extension in VS Code that can change the colors of some characters. There are plenty of those extensions. Then I made ∨ green and ∧ red

[Trebor Huang]

Is it even necessary to use a monospace font? This will not mess up the alignment if all alignments happen at the beginning of the row (with only spaces at the front). And differentiating different symbols is much easier with non-monospace fonts.

[Kayla Thomas]

Sometimes I think about inventing a language where each character is just one of the possible combinations of on and off black pixels in a m x n rectangle.
Screenshot-from-2023-07-24-21-48-43.png

[Kayla Thomas]

(deleted)

[Kayla Thomas]

I find this an interesting topic because I spent many years trying to develop a simple font (not specifically for math though).

[Mario Carneiro]

it's called QR codes

[Kayla Thomas]

oh, right.

[Kayla Thomas]

The font I was working on was not the block thing though, it was english ascii.

[Kayla Thomas]

https://github.com/pthomas505/fonts

[Kayla Thomas]

Mario Carneiro said:

it's called QR codes

In my defense, each character would be a "QR code", so not exactly the same.

[Kayla Thomas]

It's called Braille would be closer. :smile: