International docs

Stream: mathlib4

[Chris B]

Mathlib4 now has a directory for docs; I'd like to see what people think about docs in languages other than English. If there's interest, the best setup I could come up with is adding a README.md in /docs that links to external repos :

-- README.md:
Dutch : <link to Dutch doc repo>
Thai: <link to Thai doc repo>
...rest

This seems like the best option since it doesn't impose any additional maintenance overhead on mathlib, the maintainers can add/swap/remove links in a pinch, and the respective communities can manage their repos in the manner they see fit.

[Scott Morrison]

It seems at this point the additional maintenance overhead for other language documentation is zero. How likely is this to change? Couldn't we just accept PRs into mathlib4 itself?

[Chris B]

I'm not sure what the long term plans are for mathlib4 docs, but if it's something similar to the mathlib3 docs then the kind of thing I'm envisioning is that a document (e.g. the install instructions) changes and you end up with n pull requests with fixes for n languages. The mathlib3 docs files don't seem super dynamic though so that might be a concern.

[Chris B]

I guess the other extreme is that you might only get PRs for some of the languages, in which case docs that look official since they're in the repo might end up out of sync.

[Chris B]

I'm a native English speaker so this isn't like a burning issue for me; if everyone's more comfortable waiting to see if there's a more organic demand I'm good with that too.

[Patrick Massot]

I don't see how we could get forces for that.

[Patrick Massot]

One year and a half ago I made sure the natural number game could be translated (setting up a translation infrastructure). But nobody did the actual translation work. It would be much more useful than translating mathlib docs since it would allow young people to play the game (In France we have huge difficulties to get students to read English before PhD basically)

[Chris B]

Patrick Massot said:

I don't see how we could get forces for that.

I didn't mean to insinuate that this should be anyone's responsibility. The idea was more like what the Rust team did, which was to tell volunteers "if you give us a completed translation we'll make it available to visitors". I was just thinking about a folder of markdown docs, but if you're talking about like .ftl files with a structure then yeah that's going to be more work.

[Patrick Massot]

I think we're still slightly below Rust in terms of number of users...

[Patrick Massot]

I'm pretty sure I don't know any Rust user that isn't also a Lean user, but I've been told they exist.