[Noto Color Emoji] Choice to include in lean4monaco

[desaxce]

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:

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]

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]

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

[desaxce]

Thanks @joneugster, I got back to it because I faced the slow initial load once again.

I opened #4 to replace Noto with the one you created.

[desaxce]

Closing, see comments on #4