search

hhu-adam / lean4monaco

Browser support for Lean using a monaco editor.
https://www.npmjs.com/package/lean4monaco
Apache License 2.0
4 stars 1 forks source link

[Noto Color Emoji] Choice to include in lean4monaco #2

Open desaxce opened 2 months ago

desaxce commented 2 months ago

Thank your for the constant improvements!

I have a pipeline which leverages lean4monaco and automatically uses the latest published NPM package. During the week, I noticed a 10s degradation in load times for the Lean4 editor (I was in the countryside with a poor connection, but it was fast earlier last week).

It seems the introduction of the Noto Color Emoji font in e1d06209 accounts for 24MB: network

VSCode probably comes bundled with those fonts, but web browsers download them.

Could we bring down the load time by switching to a lighter font / working without it?

joneugster commented 2 months ago

Absolutely, I included the emoji font as Lean has a few emojis being used, which look bad in JuliaMono's black-and-white. Concretely its mostly about ✅, ❌ (and 💥).

If you have a suggestion for a lighter emoji font, I think we can just switch them out.

joneugster commented 2 months ago

I've tried to create my own font with just these emojis, but apparently its not compatible with some devices/browsers. That one is here:

https://github.com/hhu-adam/lean4monaco/tree/main/src/fonts/LeanWeb