Outdated wiki pages

Stream: mathlib4

[Niels Voss]

The mathlib4 GitHub wiki (https://github.com/leanprover-community/mathlib4/wiki) seems to have quite a few outdated pages, such as instructions on how to forward port changes from mathlib3 to mathlib4 and how to use #align. A lot of the info seems to be quite useful though.

What should happen to the outdated pages on porting (should they be left around for archival purposes?), and more generally, what determines whether information belongs on the GitHub wiki (as opposed to https://leanprover-community.github.io/ or library notes)?

[Jon Eugster]

I don't think there exists a clear strategy in the community about where these things belong and they grow (and rot) in an organic way. Most of the resources in all the places you linked (and more) are mostly created and managed by sporadic small efforts by (random) people, and I don't think there is a specific person or group responsible for managing these resources. I think, basically any contribution towards updating resources and organising them better is welcome!

I was hoping to automate some documentation eventually with Verso and make it easier to keep them updated that way: https://leanprover-community.github.io/mathlib-manual/html-multi/
But like any other attempt on managing ressources this is probably gonna rot too eventually ;) especially as long as verso is in active development and does not really have any documentation.

Regarding the wiki-pages concretely, I think it could be worthwhile somehow archiving anything related to Lean3 & Mathlib3. I don't know if there is a good way to do that? Probably wouldn't want to delete all of that just yet? I think there is still a reasonable (even if small) possibility that you stumble across a lean3 project and would like to have all these resources to figure out how to extract relevant parts into a more recent Lean version.

[Patrick Massot]

We still have a mathlib3 repo, so we could move all the stuff about lean 3 in the mathlib wiki to the mathlib3 wiki.

[Eric Wieser]

I think we'd have to temporarily un-archive it to do that

[Patrick Massot]

Yes, probably