[Merged by Bors] - chore(PULL_REQUEST_TEMPLATE.md): add template for moves and deletions

[jcommelin]

---

[github-actions]

PR summary 3d0ea229c3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[semorrison]

Is the intention that a bot will fill this in?

[jcommelin]

Maybe not directly filling in, but certainly the intention is that a bot will generate a first draft that can be copy-pasta-edited.

[adomani]

In particular, the pairs of declarations that decl_diff matches, are good candidates for Moves and the ones that have an unmatched - are good candidates for Deletions.

[adomani]

I looked briefly into this and I am only seeing hacky ways of getting a PR template that depends on the PR itself.

As far as I understand, GitHub simply reads the file that this PR is editing and uses that as a template. So, this file would have had to be edited between pushing and creating a PR. For instance, the very first action upon pushing could be to compute the decl_diff, modify the PR_template file and then have it ready by the time you actually open the PR!

I wonder if not git-indexing this file and simply regenerating it on every push would give the "personalised touch" that we want.

[semorrison]

I think if we develop a bot that can contribute answers here, it should just run after the PR is open. We can add a note to the template saying "You don't need to fill this in immediately: a bot will edit the PR top comment shortly with a first approximation, and you should check that it looks right."

[semorrison]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style