Pull request checklists

Stream: PhysLean

[Joseph Tooby-Smith]

I was thinking of making a github action that automatically comments on PR's with a check list of basic things that should be done/checked for in a pull-request, and maybe a question about the usage of AI. I don't want this to become an over-burden, and it is as much to ensure the quality of my own PRs as anything else.

Some examples of things may be:

• Updated the module doc-strings of any modules modified.
• Wrote comprehensive module doc-strings for new modules added.
• Ensured that theorem is used only for important theorems, otherwise used lemma.

If anyone has thoughts about what other items it would be good to include or is strongly against or for this, it would be great to hear your thoughts :).

[Kevin Buzzard]

I had FLT#418 which is probably now almost closed after FLT#424 and FLT#427 (I just didn't find the time to see which if any issues were remaining). But my checklist seems almost disjoint from yours.

[Joseph Tooby-Smith]

Yeah, looking at yours Kevin, this seems like things that there are linters to cover. I'm kind of after things which are slightly more subjective, which the linters can't cover but which would still make a good PR.

[Joseph Tooby-Smith]

This PR contains what I currently have so far in this direction:

https://github.com/HEPLean/PhysLean/pull/552

[Kevin Buzzard]

If this is a vibes thing rather than a mechanised thing then you could just make a checklist PR template like they have in core lean, they want you to tick the boxes promising that you've done various nice things before you add to their workload

[Kevin Buzzard]

Is that in fact exactly what the PR does?

[Joseph Tooby-Smith]

Yes exactly - I didn't know that the core lean has this - so will take a look at their implementation.

[Matteo Cipollina]

another possibly useful check (especially for theorems) could be adding the respective mathematical formula in Latex (with ideally a reference ) in the doc-text
and maybe also a consistent style for doc/texts. Perhaps a very dry textbook slyle 'let x be...' for docs/texts plus explanation of design choice for key defs

[Joseph Tooby-Smith]

Joseph Tooby-Smith said:

Yes exactly - I didn't know that the core lean has this - so will take a look at their implementation.

Actually sorry - not quite a PR template, but rather a bot that comments on the PR with the checklist. Maybe a template would be better.

[Joseph Tooby-Smith]

@Matteo Cipollina I would prefer if the formula was written in UTF-8 as it is readable in more/all places made for Lean (I know in some cases this is extremely hard but I think it is something we can strive for).

Maybe something like:

• For definitions and key theorems I have added, I have added an english-readable statement of the result, which is as self-contained as possible.
• Where appropriate and helpful I have included references to the original source of results.

And maybe for the first one link to some examples.