Skip to content

Conversation

@JiechengZhao
Copy link

@JiechengZhao JiechengZhao commented Mar 28, 2024

Add Translation of Chinese.

BTW, There are two

<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>
<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we-ll happily add yours.</p>

I think the second we-ll is a mistype. And now there is no i18next content use the key, so I deleted that.

@joneugster
Copy link
Collaborator

Thanks for the translations! On second thought, I think there are some instructional strings that should not be translated, e.g. the main infos on the landing page, the words "Preferences" and "Impressum", ... Or at least I shoudl check with uni if these things should stay in english

Therefore I merged this manually! If you rebase this PR to dev, then it shows the translations I deleted for the time being.

@joneugster
Copy link
Collaborator

(about the misstype, appartenly i18next-scanner did not delete the unused key. Maybe I can change the settings so that it does)

@JiechengZhao
Copy link
Author

JiechengZhao commented Mar 31, 2024

@joneugster, currently identified 4 points:

  1. The "Start" button in the intro panel was not translated. This has been addressed in commit 470a184.
  2. The "Goal" and "Objects" in Goal component. Fixed in af54268
  3. The level names remain untranslated. Their names have not yet been extracted as keys.
    Screenshot from 2024-04-01 13-16-01
  4. The level completed! 🎉 in the Error box.
    Screenshot from 2024-04-01 13-15-43

joneugster added a commit that referenced this pull request Apr 9, 2024
@joneugster
Copy link
Collaborator

  1. has been fixed in 9b05a27
  2. Is a bit trickier (as rn these are generated in the lean server), but I implemented a hack so that the message "level completed!" appears in the Game's .pot file and can be translated there. Needs a better solution long-term.

I think I added all changes from this PR manually. The only things that should be left, are the translations of

  • Impressum
  • Preferences
  • The landing page

As I'm not fully sure of the implications of having the server located in Germany and having these text in a language different than German or English. But I'd leave your PR here, so these translations could be added later.

@joneugster joneugster changed the base branch from dev to main April 9, 2024 07:54
@joneugster joneugster changed the base branch from main to dev April 9, 2024 07:54
@joneugster
Copy link
Collaborator

I think if you rebase @JiechengZhao , you should see that only few diffs remain

@JiechengZhao
Copy link
Author

I think if you rebase @JiechengZhao , you should see that only few diffs remain

Hi, I have rebased the code, and it looks good. Currently, I cannot generate new Game.pot or Game.json files with new keys based on the new lean4game branch. Which command will do the job? I thought you have mentioned but I cannot find it.

@joneugster
Copy link
Collaborator

joneugster commented Apr 10, 2024

lake build does it at the end automatically, but otherwide lake exe i18n -t does this manually. (both in the nng repo)

in the lean4game repo, npm run translate will update the translation json files and give you an overview if it added or removed anything.

I think by the end of the week I will have integrated all these pieces, added the docs and updated NNG4 to use the new version completely. then I'll creat the v4.7.0 release of lean4game

@JiechengZhao
Copy link
Author

@joneugster Please check and merge this P.R. There are still some scripts in server to update.

@joneugster
Copy link
Collaborator

ok, talked to my group. If we add the word "Impressum" in English, we can merge all of these changes, too!

@JiechengZhao
Copy link
Author

ok, talked to my group. If we add the word "Impressum" in English, we can merge all of these changes, too!

Cool. I also finished my test, so I think it is ready to merge.

@joneugster joneugster merged commit 3ddcc35 into leanprover-community:dev Apr 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants