search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
174 stars 29 forks source link

`lake exe i18n --export-json` does not support `#~` #210

Closed JiechengZhao closed 3 months ago

JiechengZhao commented 5 months ago

`lake exe i18n --export-json failed on https://github.com/JiechengZhao/NNG4/commit/d4d1e19f13f58263df5790c33dd6621d9aac0b2a .

jiecheng@jiecheng-Vostro-3420:~/workspace/lean/lean4games/NNG4$ lake exe i18n --export-json
PANIC at I18n.POFile.read I18n.PO.Read:289:4: Failed to parse PO file: offset 200468: unexpected comment format.
backtrace:
./.lake/packages/i18n/.lake/build/bin/i18n(lean_panic_fn+0x9e)[0x616baa681a4e]
./.lake/packages/i18n/.lake/build/bin/i18n(l_I18n_POFile_read___lambda__1+0x365)[0x616ba74a94a5]
./.lake/packages/i18n/.lake/build/bin/i18n(l_Array_forInUnsafe_loop___at_I18n_i18nCLI___spec__1+0xcd)[0x616ba74b7ebd]
./.lake/packages/i18n/.lake/build/bin/i18n(l_I18n_i18nCLI___lambda__2+0x120)[0x616ba74b8480]
./.lake/packages/i18n/.lake/build/bin/i18n(l_I18n_i18nCLI+0x7c)[0x616ba74b8ddc]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x136)[0x616baa68cef6]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x571)[0x616baa68d331]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x2ad)[0x616baa68d06d]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x2ad)[0x616baa68d06d]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x2ad)[0x616baa68d06d]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x2ad)[0x616baa68d06d]
./.lake/packages/i18n/.lake/build/bin/i18n(lean_apply_2+0x2ad)[0x616baa68d06d]
./.lake/packages/i18n/.lake/build/bin/i18n(+0xc2362d)[0x616ba743c62d]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x731e04a29d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x731e04a29e40]
./.lake/packages/i18n/.lake/build/bin/i18n(_start+0x25)[0x616ba743b7a5]
uncaught exception: already exists (error code: 0, )

The content is 

#~ msgid ""\n#~ "## Sum'

#~ is generated by msgmerge (gettext) when it finds that an old script does not match or only fuzzily matches the current key. Deleting this part is okay, but since this is a common behavior in gettext, adding support for it would be good.

joneugster commented 5 months ago

I'll add that later this week.

My manual https://www.gnu.org/software/gettext/manual/gettext.html#PO-Files (or at least not in the obvious section. didn't read anything about msgmerge yet) did not include that syntax, but if POEdit does, we should add it too. That should be easy, just adding this case in the PO-parser.

JiechengZhao commented 5 months ago

I'll add that later this week.

My manual https://www.gnu.org/software/gettext/manual/gettext.html#PO-Files (or at least not in the obvious section. didn't read anything about msgmerge yet) did not include that syntax, but if POEdit does, we should add it too. That should be easy, just adding this case in the PO-parser.

I guess the gettext manual missed it in the PO files description. It is in the utils and the manual mentioned it here: https://www.gnu.org/software/gettext/manual/gettext.html#Message-selection-4 . I can only use search to find that. It's not even mentioned in all other utils. :scream: .

joneugster commented 3 months ago

Sorry, forgot about this. The parser should now just drop them.