How to use i18n in Lean4Game

Stream: general

[ZHAO Jiecheng]

@Jon Eugster Hi, I have prepared a .po file in NNG4 to translate it into Chinese. How can I use the lean-i18n to generate the Chinese version of NNG4, though I know there are some front-end codes not ready. But I can also code js or ts. So maybe I can help. I can also program in Lean, but know little meta programming unfortunately.

https://github.com/JiechengZhao/NNG4/tree/main/.i18n

I really hope that more Chinese users can play the lean games.

[Jon Eugster]

Amazing!

You should PR this to the NNG4 repo, going to ./i18n/Game-zh.po (or ./i18n/Game-zh_CN.po or whatever the correct ISO language code is.)

On the front-end side nothing has been done so far. If you wanted to help implement that, first thing is adding a npm module which supports using PO files. I think i18next or react-intl are canonical choices for internationalisation packages, but that's where I lack experience (and why I did other stuff instead).

Once that's set-up it should be easy to use the translation everywhere in the game.

[ZHAO Jiecheng]

Jon Eugster said:

Game-zh_CN

PR raised
https://github.com/leanprover-community/NNG4/pull/55

[ZHAO Jiecheng]

@Jon Eugster Also report some bugs. https://github.com/leanprover-community/NNG4/issues/56 There are some small bugs in the generated pot, which also means bugs in lean-i18n. the bugs can be auto fixed by software like Poedit. but will cause error in msginit.

[Jon Eugster]

Thanks, Ill look at it.

I'll probably move the issue about i18n to
https://github.com/hhu-adam/lean-i18n

[ZHAO Jiecheng]

Jon Eugster said:

Thanks, Ill look at it.

I'll probably move the issue about i18n to
https://github.com/hhu-adam/lean-i18n

yes, that is more reasonable.

[ZHAO Jiecheng]

User
@Jon Eugster Here is another PR. I added react_i18next and set it up.
https://github.com/leanprover-community/lean4game/pull/203

[Bulhwi Cha]

@ZHAO Jiecheng I think now I can start translating NNG4 into Korean thanks to you! I really appreciate it.