gettext?

Stream: Is there code for X?

[Jz Pan]

Do you think a pure Lean version of GNU GetText will be useful? It is used for internationalization.

If there are anyone interested in it, I may work on it (low priority).

[Mario Carneiro]

I recall @Patrick Massot thinking about this question for Verbose Lean, I forget where he ended up

[Mario Carneiro]

I think it was not directly reimplemented but something equivalent can be done using lean metaprogramming

[Jz Pan]

The parsing of .mo files is easy, I've written implementations for different languages before

[Mario Carneiro]

I think the issue was more that the way gettext works doesn't jive so well with lean, it's more suitable for languages that rely on external code generation like C

[Jz Pan]

Mario Carneiro said:

I think the issue was more that the way gettext works doesn't jive so well with lean, it's more suitable for languages that rely on external code generation like C

I don't get the point yet... We can also define GetText.gettext (self : GetText) (s : String) : String which works exactly like in other languages.

[Jz Pan]

Of course it's best if we have Lean specific version of xgettext which scans the source code using Lean's built-in metaprogramming ability.

[Patrick Massot]

The multilingual support in Verbose Lean does a lot more that translating strings, but it’s also more work to use. It is described in the paper and the main code is at https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/Infrastructure/Multilingual.lean. As you can see on line 1 of that file, this is all due to Mario.

[Jz Pan]

Well, personally I think it's too cumbersome to use. Seems that for each internationalized function you need to implement it in each language.

[Patrick Massot]

You only need to implement it for language that want to use it. But it’s a lot more flexible than replacing a string by another string.

[Jon Eugster]

I've started parsing of .po files according to GNU gettext like 2 years ago here: https://github.com/hhu-adam/lean-i18n
This is also used in NNG etc.

Probably worth if you had a look at that and see if it could be a possibility to contribute improvements to that project before implementing everything from scratch again :)

I would love to see that package be improved futher!

[Jz Pan]

Jon Eugster said:

I've started parsing of .po files according to GNU gettext like 2 years ago here: https://github.com/hhu-adam/lean-i18n
This is also used in NNG etc.

Probably worth if you had a look at that and see if it could be a possibility to contribute improvements to that project before implementing everything from scratch again :)

I would love to see that package be improved futher!

Great work! I'll check it. I have written .mo file parsing and plural forms (with an expression parser) in other programming languages before.