Lean specific font

Stream: general

[Jon Eugster]

Bit of a random question... There are some symbols that Lean actively uses in the infoview:

• ✝ for inaccessible variables
• 🎉 for "success"
• ❌✅💥▼▶: for debugging in set_option trace.Meta.synthInstance true, for example in:

[Meta.synthInstance] ❌ Decidable (sorryAx Prop true) ▼

  [] no instances for Decidable (sorryAx Prop true) ▶

These can be messed up by custom fonts, for example when the font defines ✝ as an Emoji, or if ✅ is not an emoji but instead monochrom.

Do you know of any other such "control"-symbols used by (debugging-) tools in Lean/Mathlib?

[Johan Commelin]

I can't think of any others right now. What do you need this for, if I may ask?

[Damiano Testa]

Does the coercion up-arrow count?

[Jon Eugster]

I changed the web editor to JuliaMono a while ago which had the disadvantage that ❌✅ where black-and-white (which is not ideal for visability), and adding any emoji font rendered ✝ as a huge purple box.

So I created a new font with only these few symbols, and I thought since I already have the app open, I might ask here about symbols that might not work well in certain fonts.

[Eric Wieser]

Jon Eugster said:

or if ✅ is not an emoji but instead monochrom.

This sounds like an infoview thing; there is a CSS way to say "prefer emoji rendering for this character"

[Jon Eugster]

Indeed this is mostly about fonts in the infoview.

Is there? I know CSS font-variant-emoji but that looks to me like you'd have to wrap the specific unicode characters first (with JS?) or make that changes at the source where that character is printed.

[Eric Wieser]

Are the emojis not already handled specially by the trace tree view?

[Eric Wieser]

Apparently inserting \uFE0F before the emoji forcing it to render as the colored version

[Eric Wieser]

(also as an aside, it's totally nuts that I found this out through a webpage with an embedded VNC client running Tcl)

[Jon Eugster]

But that's the thing, on my device all the 3 rows look the same. Presumably because I don't have the correct fonts installed :man_shrugging:

[Eric Wieser]

The page is bad, they look the same because VNC doesn't support the feature

[Eric Wieser]

#eval "|\uFE0F✅,\uFE0E✅,✅|"
#eval "|\uFE0F❌,\uFE0E❌,❌|"

should be a good test. The web editor indeed doesn't support it

[Eric Wieser]

https://www.codejam.info/2021/11/emoji-variation-selector.html is a better reference

[Julian Berman]

Hrm, that doesn't seem to work in Kitty, even though it definitely supports variation selection.

[Julian Berman]

Oh, it's in the wrong spot I think? It seems like it goes after, and should be

#eval "|✅\uFE0F,✅\uFE0E,✅|"
#eval "|❌\uFE0F,❌\uFE0E,❌|"

[Julian Berman]

Which now works in the web editor too seemingly.

[Eric Wieser]

Julian Berman said:

Which now works in the web editor too seemingly.

Not for me on windows

[Jon Eugster]

how does this look like for you? demo

[Eric Wieser]

The characters are completely missing for me

[Eric Wieser]

(and the lean server never starts, and the button to start it is missing)

[Julian Berman]

Screenshot-2024-08-12-at-12.53.56.png

macOS + FF latest beta

[Jon Eugster]

Eric Wieser said:

The characters are completely missing for me

I have that on Android, too. so somethings off there.

[Jon Eugster]

Eric Wieser said:

(and the lean server never starts, and the button to start it is missing)

As in, you never get the infoview?

[Eric Wieser]

I don't think you're serving the font files to me at all?

[Eric Wieser]

Yes, the infoview says "Waiting for Lean server to start...". This happens all the time in the live editor too, but there I can restart the server.

[Jon Eugster]

Eric Wieser said:

I don't think you're serving the font files to me at all?

Oh that might be. They might be served inside the infoview (which is inside an iframe) maybe need to serve them outside, too

[Eric Wieser]

That might be related to the infoview not loading for me

[Jon Eugster]

Eric Wieser said:

That might be related to the infoview not loading for me

do you get anything in the console?

[Eric Wieser]

VM722:1 Uncaught SyntaxError: Unexpected token 'e', "esms,true,"... is not valid JSON
    at JSON.parse (<anonymous>)
    at webview.js:1:39057

and also

[InfoProvider] initInfoView got null client.

[Jon Eugster]

Eric Wieser said:

VM722:1 Uncaught SyntaxError: Unexpected token 'e', "esms,true,"... is not valid JSON
    at JSON.parse (<anonymous>)
    at webview.js:1:39057

This one I already addressed locally, but so far my browsers where quiet happily ignoring it.

Thanks, I'll have a look!

[Jon Eugster]

So do you think it would be desirable to make a PR for the infoview to change in particular ✝ to ✝\uFE0E? Or is that only making it the unicode situation even worse?

[Joachim Breitner]

Depends on what gets worse. If users copy and paste that into the edit pane, does the variant selector also get copied?

[Eric Wieser]

I think the variant selector and the codepoint before it is treated as a single character by the monaco editor

[Jon Eugster]

I created lean#5015 for the team to consider. Although I understand that's not a pressing issue at all.

I'll work with whatever the decision there is :smiling_face: