documentation TODOs

Stream: mathlib4

[Jireh Loreaux]

When I migrated the README in #6160 I took out some links that were in the mathlib3 version that were specific to Lean 3. This is different than just pages on the website not being updated. I think we need a plan for some of these.

The things I removed were:

---

from the documentation section:

In addition to the pages generated for each file in the library, the docs also include pages on:

- tactics,
- commands,
- hole commands, and
- attributes.
- A couple of tutorial Lean files

from the guidelines section:

• The commit naming conventions

---

In particular, I think we need:

1. A new commit naming convention file (or webpage on the community site), although the precise outcome is not exactly clear to me from this discussion; the poll went one way, but then it seemed there was some support for a compromise at the end of the thread. If we can come to a conclusion there, I can create this file/page and link it from the readme.
2. A way to list tactics, commands, hole commands and attributes, even if it means we have to manually tag things. I know we have #help, and while that's handy especially when you're in the middle of something, it's not as nice as the lists we had in Lean 3 on the website.

[Kevin Buzzard]

(the "tutorial Lean files" link is broken)

[Jireh Loreaux]

oops, fixed. It was a relative markdown link to a file in the mathlib3 repo.

[Jireh Loreaux]

I think a suitable replacement for the tutorial files may be #mil

[Kevin Buzzard]

Thanks for fixing the link: I couldn't reconstruct it myself. I wrote some of those files way back when there was only TPIL. If you think that porting them is not necessary then that's fine. Nowadays I write files like that in my undergraduate course repo which I will be porting to mathlib4 in December or so.

[Mario Carneiro]

BTW, the updated README no longer links to the porting wiki. Although the port is "done", I think a lot of information on the wiki is still relevant for people porting mathlib PRs, porting external projects in mathlib style, and for people learning how to code in mathlib4 from lean 3 experience

[Mario Carneiro]

it's possible we might want to adjust the content of the wiki to focus more on these use cases though

[Jireh Loreaux]

I did add a section which links to the survival guide and mathport, but the porting wiki could be useful too.