Where can I find the latest source code of Lean homepage?

Stream: general

[Oling Cat]

Hi there, I want translate Lean homepage into Chinese. I found a repo on Github but there is just an indirect link into homepage. Where should I go to find the latest homepage source code?

[Utensil Song]

It's in a private repo, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Verso.3A.20could.20not.20execute.20external.20process for why.

[Kim Morrison]

Please don't make copies of the Lean homepage. If you would like to contribute translations to the community Lean webpage that would probably be welcome.

[Oling Cat]

Utensil Song said:

It's in a private repo, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Verso.3A.20could.20not.20execute.20external.20process for why.

Thank you.

[Oling Cat]

Kim Morrison said:

Please don't make copies of the Lean homepage. If you would like to contribute translations to the community Lean webpage that would probably be welcome.

How to contribute a Chinese translation for homepage? By the way, we are translating Functional Programming in Lean and Theorem Proving in Lean. Should I merge it into the official repo?

[Oling Cat]

I just opened an issue at How to contribute a Chinese translation for homepage? · Issue #115 · leanprover/leanprover.github.io

[Utensil Song]

#fpil and #tpil are in separate public repos, they are just deployed to the same domain as the home page. Lean 4 manual is also in public repo inside Lean 4's repo.

[Utensil Song]

You'll need to ask for translation permissions from different authors, so the authors of these books will be aware of (and give explicit consent to) the existence of translation, maybe provide official links to the translations in different languages.

It's better to maintain the translation of these books in different repos, 1:1 with the original repo, keep the English version in the translated repo and add Translations to other directories to avoid merge confliction.

Then you may have a Lean 4 Chinese community homepage to link to these resources. The Lean 4 home page as of now has little to nothing to translate, mostly only the various resources it links to are worth translating. One exception is the blog posts authored in Verso, which I hope to become in public repo one day.

The community website has many things worth translating, but it's also updated frequently, one issue is that you need to be able to detect changes of each page and request translators to catch up.