Project: Dutch version of verbose-lean4

Stream: Lean for teaching

[Johan Commelin]

Hoi allemaal!

Spreek je nederlands, en ben je fan van Patrick Massot's verbose-lean4 controlled-natural-language tactics? Help dan mee om een nederlandse versie te maken.

Ik heb een beginnetje gemaakt op https://github.com/jcommelin/verbose-lean4/tree/dutch

Als je mee wilt helpen, reageer dan op dit bericht, dan geef ik je push-access op deze repo. Wanneer we klaar zijn met de vertaling kunnen we een PR maken naar de originele repo van Patrick.

[Johan Commelin]

Bij sommige vertalingen heb ik niet het gevoel dat ik de optimale keuze heb gemaakt. Dus feedback op mijn vertalingen/keuzes is van harte welkom!

[Floris van Doorn]

I am considering to write a German version over the next year...

[Pietro Monticone]

You can find the Italian version I am working on here.

[Patrick Massot]

You should not need to fork the library to write a version in your own language. You should import it in your library. If this isn’t sufficient then you should tell me about this issue.

[Patrick Massot]

Note that I’m currently working on porting my Lean 3 course to Lean 4 and this will probably uncover issues with the Lean 4 version of the library. Hopefully this will be done this week (ideally before my talk on Wednesday but this isn’t guaranteed).

[Johan Commelin]

But if we want to upstream the translations, then we would need a fork, right?

[Chris Henson]

Johan Commelin said:

But if we want to upstream the translations, then we would need a fork, right?

I feel like different meanings/connotations of "fork" create confusion here. Sometimes it means you're splitting off the repo into something that is your own and diverging. Other times, especially on GitHub, you are just using it logistically the same way you would a branch, with the intent of upstreaming.

[Patrick Massot]

If you want to upstream your translation then you need to promise to (try) to maintain it whenever the main library changes. Because I won’t be able to maintain a Dutch (or even German) version. If you keep it separated then you can simply pin the dependency version and update it when you have time.