RFC: Use emoji variant selector for unicode characters

[joneugster]

Proposal

Occasionally, Lean uses emojis, for example it uses ✅❌💥 for debugging. The proposal is to use the variant selector with \uFE0F followed:

In particular, use

emoji variant: ✅️❌️💥️
text variant: ✝︎▼︎▶︎

(which look the same, but are different to the currently used ✅❌💥✝▼▶)

User Experience

Minor improvement, but helps with using custom fonts. See for example live.lean-lang.org:

set_option trace.Meta.synthInstance true

#synth Decidable Nat

which displays

[Meta.synthInstance] ❌︎ CoeT Type Nat Prop ▼
  [] new goal CoeT Type Nat Prop ▶
  [] ❌︎ apply @instCoeT to CoeT Type Nat Prop ▶
  [] ✅︎ apply @instCoeTOfCoeDep to CoeT Type Nat Prop ▶
  [] ✅︎ apply @instCoeTOfCoeHTCT to CoeT Type Nat Prop ▶
  [] ❌︎ apply @instCoeHTCT to CoeHTCT Type Prop ▶
  [] ✅︎ apply @instCoeHTCTOfCoeHTC to CoeHTCT Type Prop ▶
  [] ❌︎ apply @instCoeHTC to CoeHTC Type Prop ▶
  [] ✅︎ apply @instCoeHTCOfCoeOTC to CoeHTC Type Prop 

instead of

[Meta.synthInstance] ❌️ CoeT Type Nat Prop ▼
  [] new goal CoeT Type Nat Prop ▶
  [] ❌️ apply @instCoeT to CoeT Type Nat Prop ▶
  [] ✅️ apply @instCoeTOfCoeDep to CoeT Type Nat Prop ▶
  [] ✅️ apply @instCoeTOfCoeHTCT to CoeT Type Nat Prop ▶
  [] ❌️ apply @instCoeHTCT to CoeHTCT Type Prop ▶
  [] ✅️ apply @instCoeHTCTOfCoeHTC to CoeHTCT Type Prop ▶
  [] ❌️ apply @instCoeHTC to CoeHTC Type Prop ▶
  [] ✅️ apply @instCoeHTCOfCoeOTC to CoeHTC Type Prop 

Further, using the wrong font, one might see inst✝️ instead of inst✝︎, which is distracting.

Beneficiaries

Better support for custom fonts helps in particular the international community as for example Chinese, Japanese or Cyrillic script might require usage of a custom font. E.g. JuliaMono is defacto a solid choice and also used by live.lean-lang.org.

Maintainability

There is some potential issue to consider about unicode characters that look identical.

Community Feedback

There was some private feedback by Joachim Breitner (@nomeata) that ❌︎ and ✅︎ in the trace output is not nice as they are harder to recognise.

Zulip discussion suggests this could be a valid approach if it doesn't create new pitfalls for the user.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

RFC accepted

[nomeata]

@joneugster, do you plan to implement this as well?

[joneugster]

Thanks for looking at the rfc. I can create an implementation next week if that's desired👍

[nomeata]

Thanks!