Unicode spec proposal for PL implementers

Stream: general

[Mario Carneiro]

Unicode has just come out with a specification for programming languages and editor implementers with recommendations for source code: what is allowed, how things are displayed, and what diagnostics should be used for things like bidirectional text and confusables. The proposed specification is here: https://www.unicode.org/reports/tr55/proposed.html , and you can submit feedback to https://www.unicode.org/review/pri474/ .

(This is not directly lean related, but there might be things we might want to influence there, as well as conversely recommendations we should adopt into lean tooling, since we do use a lot of unicode.)

[Eric Wieser]

Wow, maybe unicode source code is cursed after all