PR summary 3d0ea229c3

Import changes for modified files

No significant changes to the import graph

Declarations diff

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

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

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

Is the intention that a bot will fill this in?

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

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.

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.

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."

bors merge

Build failed (retrying...):

• Build

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style