Use stale bot to close old pull requests

Should we automatically close stale pull request on GitHub?

Some GitHub users won't contribute to a project with lots of open pull requests, because they think it's been abandoned. (Or they think we're bad at merging PRs.)

But lots of our PRs get left open because we've squashed and merged the PR, and GitHub doesn't recognise the squashed commits, so GitHub doesn't auto-close the PR.

Closing a PR:

• hides it from the default list of PRs
• hides its CI results in the PR itself (but they still appear in the PR list)

Anyone can reopen a closed PR. Re-opening a PR re-runs CI (which is usually what we want for old PRs).

I suggest we use probot stale: https://probot.github.io/apps/stale/

With the following options:

• daysUntilStale: 60
  • some backport PRs are older than 60 days, but their CI should have been checked when they were reviewed
  • we don't merge very many stale PRs to master
  • any period from 30 days (most reviews completed) to 6 months (release cycle) would probably work for us
• daysUntilClose: 7
• exemptLabels: pinned
• staleLabel: stale-closed
• markComment: (like the suggested one, but mention the "pinned" label)
• closeComment: false

On the following network team repositories:

• tor
  • ~400 older than 2 months
  • ~270 older than 6 months
• torspec
  • 8 older than 2 months
  • 6 older than 6 months
• chutney
  • 1 older than 6 months, needs to be pinned?
• fallback-scripts

And the top-level GitHub config repository:

• .github