localization

Stream: general

[Kenny Lau]

can we have a Spanish Lean / VSCode environment?

[Johan Commelin]

Probably requires you to translate a lot of stuff.

[Kenny Lau]

Can we set something up so that we can have a progress bar on translations and everyone can contribute?

[Simon Hudon]

Also consider that new features come in fast and you'll have translate it as it come in so that those versions don't lag behind

[Kenny Lau]

maybe just Spanish VSCode then, I suppose programming languages don't get translated to other languages

[Simon Hudon]

If you only translate VS code, the error messages are still in english, that is most of the interactive experience, isn't it?

[Kenny Lau]

hmm

[Johan Commelin]

Unison gives every declaration a canonical name (the hash of the declaration) and then has tables with names pointing to hashes. It can "elaborate" the names away and "delaborate" them back. This makes for very easy translating into other languages!

[Johan Commelin]

Are you sure coding in lean is the best way to improve your spanish?

[Kenny Lau]

oh VSCode already has Spanish (Ctrl+Shift+P > configure display language)