gh-35172: New workflow for synchronization of labels

    
<!-- ^^^^^
Please provide a concise, informative and self-explanatory title.
Don't put issue numbers in there, do this in the PR body below.
For example, instead of "Fixes #1234" use "Introduce new method to
calculate 1+1"
-->
### 📚 Description

<!-- Describe your changes here in detail -->
<!-- Why is this change required? What problem does it solve? -->
<!-- If it resolves an open issue, please link to the issue here. For
example "Closes #1337" -->

This PR is a continuation of https://github.com/sagemath/trac-to-
github/pull/187.

It implements GitHub actions to synchronize the labels migrated from
Trac selection lists (according to issue
sagemath/trac-to-github#117). These are the
priority and state labels (type labels are not considered here since
their meaning has changed).

The bot will not be active immediatly after this PR is merged. It needs
to be activated by a maintainer of the repository by adding the variable
`SYNC_LABELS_ACTIVE` with value `yes` under

```
Settings -> Secrets and variables -> Actions
```

At the moment the script takes care that there is just one item present
from each list and it sets `s: needs review` on a non draft PR opening.
Furthermore, it reacts on review approval and change requests setting
according labels automatically (after some checks). Conversely, setting
a state label will lead to automatic approval resp. change request under
certain circumstances. If there is need to reject it a warning comment
is posted.

For a detailed description of the workflows see the flowcharts below. In
summary, the bot keeps the meaning consistent along the rows in the
table below:

| Trac status | GH label | closed | draft | review decision |
| - | - | - | - | - |
| new |  | No | Yes | None |
| needs_info | s: needs info | No | No / Yes | Any |
| needs review | s: needs review | No | No | Any |
| needs work | s: needs work | No | No | CHANGES REQUESTED |
| positive review | s: positive review | No | No | APPROVED |
| closed |  | Yes | No / Yes | Any |

The review decision is not given explicitly on all cases. Implicitly it
can be read of the list of all reviews. So if there is at least one
review requesting changes younger than any commit the review decision is
interpreted as `CHANGES REQUESTED`. If there is at least one approved
review younger than any commit but none requesting changes the review
decision is interpreted as `APPROVED`.


Please consider this implementation just as a base of discussion.

#### Open problems and questions

* At the moment there is no synchronization between issue labels of
selection lists and corresponding labels of associated PRs
* Does it make sense to have state labels on issues? In the current
version of the PR I reject all but `s: needs info`.
* In general the relation between issues and PRs can be n:m. Shall we
accept different priorities among them or shall we put all these to the
maximum. I think at least the priority of a PR should be the maximum of
all issues fixed by it.

#### Notes on testing

The failure of the *Synchronize selection list labeled / synchronize
(pull_request)* check is to be expected (see
#35172 (comment))
since it is trying to download the python file from the upstream
repository (`sagemath/sage`). Therefore testing the script must be done
relative to my fork (`soehms/sage`). First examples are
soehms#1 and
soehms#2. It would be helpful if others
would open PRs there in order to test the review functionality which I
can't do by myself.


### Flowcharts

#### What happens when a PR changes its state?

##### What happens when a PR is opened?

```mermaid
---
title: open a PR
---
flowchart LR

%% vertices

    trigger([open\n])
    add_needs_review(['s: needs review'\n label added])
    nothing([do nothing])
    is_draft{is PR\n a draft?}

%% edges

    trigger ---> is_draft
    is_draft -- true ---> nothing
    is_draft -- false ---> add_needs_review
```



##### What happens when a PR is closed or reopened or converted to a
draft?

```mermaid
---
title: close, reopen or convert a PR to a draft
---
flowchart LR

%% vertices

    trigger([close, reopen or\n convert to draft])
    remove_all_labels([remove all\n state labels])

%% edges

    trigger ---> remove_all_labels
```

##### What happens when a draft is ready for review or the branch of a
PR is synchronized?

```mermaid
---
title: draft ready for review or branch synchronized
---
flowchart LR

%% vertices

    trigger([ready for\n review])
    nothing([do nothing])
    add_needs_review(['s: needs review'\n label selected])
    needs_review_valid[[needs review\n valid?]]

%% edges

    trigger ---> needs_review_valid
    needs_review_valid -- true ---> add_needs_review
    needs_review_valid -- false ---> nothing
```

```mermaid
---
title: needs review valid?
---
flowchart LR

%% vertices

    needs_review_valid([needs review\n valid?])
    true([true])
    false([false])
    needs_work_valid[[needs work\n valid?]]
    positive_review_valid[[positive review\n valid?]]
    is_draft{is PR\n a draft?}

%% edges

    needs_review_valid ---> is_draft
    is_draft -- yes ---> false
    is_draft -- no ---> needs_work_valid
    needs_work_valid -- true ---> false
    needs_work_valid -- false ---> positive_review_valid
    positive_review_valid -- true ---> false
    positive_review_valid -- false ---> true
```

```mermaid
---
title: needs work valid?
---
flowchart LR

%% vertices

    needs_work_valid([needs work\n valid?])
    true([true])
    false([false])
    proper_review_exists{proper review\n after most recent\n commit
exists?}
    review_decision_exists{review\n decision\n exists?}
    review_decision_request_changes{review\n decision is\n CHANGES\n
REQUESTED?}
    any_review_request_changes{any proper\n review requests\n changes?}

%% edges

    needs_work_valid  --> proper_review_exists
    proper_review_exists -- yes ---> review_decision_exists
    proper_review_exists -- no ---> false
    review_decision_exists -- yes ---> review_decision_request_changes
    review_decision_exists -- no ---> any_review_request_changes
    review_decision_request_changes -- yes --> true
    review_decision_request_changes -- no --> false
    any_review_request_changes -- yes ---> true
    any_review_request_changes -- no ---> false
```

Here, proper means that the review is more than a comment.


```mermaid
---
title: positive review valid?
---
flowchart LR

%% vertices

    positive_review_valid([positive review\n valid?])
    true([true])
    false([false])
    proper_review_exists{proper review\n after most recent\n commit
exists?}
    review_decision_exists{review\n decision\n exists?}
    review_decision_approved{review\n decision is\n APPROVED?}
    all_proper_reviews_approved{all proper\n reviews\n approved?}

%% edges

    positive_review_valid  --> proper_review_exists
    proper_review_exists  -- yes ---> review_decision_exists
    proper_review_exists  -- no ---> false
    review_decision_exists -- yes ---> review_decision_approved
    review_decision_exists -- no ---> all_proper_reviews_approved
    review_decision_approved -- yes --> true
    review_decision_approved -- no --> false
    all_proper_reviews_approved -- yes ---> true
    all_proper_reviews_approved -- no ---> false
```

Here, proper means that the review is more than a comment.


##### What happens when changes are requested for a PR?

```mermaid
---
title: request changes
---
flowchart LR

%% vertices

    trigger([request\n changes\n])
    add_needs_work(['s: needs work'\n label selected])
    nothing([do nothing])
    needs_work_valid[[needs work\n valid?]]

%% edges

    trigger ---> needs_work_valid
    needs_work_valid -- true ---> add_needs_work
    needs_work_valid -- false ---> nothing
```


##### What happens when a PR is approved?

```mermaid
---
title: approve
---
flowchart LR

%% vertices

    trigger([approve\n])
    select_positive_review(['s: positive review'\n label selected])
    nothing([do nothing])
    positive_review_valid[[positive review\n valid?]]
    actor_authorized{is actor\n a member of\n Triage?}

%% edges

    trigger ---> actor_authorized
    actor_authorized -- yes ---> positive_review_valid
    actor_authorized -- no ---> nothing
    positive_review_valid -- true ---> select_positive_review
    positive_review_valid -- false ---> nothing
```


#### What happens when state or priority labels are changed?

##### What happens when adding `s: positive review` to a PR?

```mermaid
---
title: add the positive review label
---
flowchart LR

%% vertices

    trigger([label\n 's: positive review'\n added])
    positive_review_valid[[positive review\n valid?]]
    approve_pr([approve])
    remove_other_labels([remove other\n state labels])
    approve_allowed[[approve\n allowed?]]
    reject_label_addition[[reject\n label\n addition]]

%% edges

    trigger --> positive_review_valid
    positive_review_valid -- yes ---> remove_other_labels
    positive_review_valid -- no ---> approve_allowed
    approve_allowed -- yes ---> approve_pr
    approve_allowed -- no ---> reject_label_addition
    approve_pr --> remove_other_labels
```

```mermaid
---
title: approve allowed?
---
flowchart LR

%% vertices

    trigger([approve\n allowed?])
    true([true])
    false([false])
    review_of_member_exists{review\n of a member\n exists?}
    review_of_others_request_changes{changes\n requested by\n someone\n
else exists?}
    actor_valid[[actor valid?]]

%% edges

    trigger --> review_of_member_exists
    review_of_member_exists -- yes ---> review_of_others_request_changes
    review_of_member_exists -- no ---> false
    review_of_others_request_changes -- yes ---> false
    review_of_others_request_changes -- no ---> actor_valid
    actor_valid -- yes ---> true
    actor_valid -- no ---> false
```

Here, only reviews of someone else are considered which are more recent
than any commit.


```mermaid
---
title: actor valid
---
flowchart LR

%% vertices

    actor_valid([actor valid?])
    true([true])
    false([false])
    actor_is_author{actor is\n author?}
    other_reviews{reviews of\n someone else\n exists?}
    other_commits{commits of\n someone else\n exists?}

%% edges

    actor_valid  --> actor_is_author
    actor_is_author -- yes ---> other_reviews
    actor_is_author -- no ---> true
    other_reviews -- yes ---> other_commits
    other_reviews -- no ---> false
    other_commits -- yes ---> true
    other_commits -- no ---> false
```

```mermaid
---
title: reject label addition
---
flowchart LR

%% vertices

    reject_label_addition([reject\n label\n addition])
    add_warning_comment([add\n warning\n comment])
    remove_label([remove label])

%% edges

    reject_label_addition  --> add_warning_comment
    add_warning_comment  --> remove_label
```


##### What happens when adding `s: needs work` to a PR?

```mermaid
---
title: add the needs work label
---
flowchart LR

%% vertices

    trigger([label\n 's: needs work'\n added])
    request_changes([request changes])
    remove_other_labels([remove other\n state labels])
    reject_label_addition[[reject\n label\n addition]]
    needs_work_valid[[needs work\n valid?]]
    is_draft{is PR\n a draft?}

%% edges

    trigger --> needs_work_valid
    needs_work_valid -- true ---> remove_other_labels
    needs_work_valid -- false ---> is_draft
    is_draft -- yes ---> reject_label_addition
    is_draft -- no ---> request_changes
    request_changes --> remove_other_labels
```

##### What happens when adding `s: needs review` to a PR?

```mermaid
---
title: add the needs review label
---
flowchart LR

%% vertices

    trigger([label\n 's: needs review'\n added])
    mark_as_ready([mark as\n ready for\n review])
    remove_other_labels([remove other\n state labels])
    reject_label_addition[[reject\n label\n addition]]
    needs_review_valid[[needs review\n valid?]]
    is_draft{is PR\n a draft?}

%% edges

    trigger --> needs_review_valid
    needs_review_valid -- true ---> remove_other_labels
    needs_review_valid -- false ---> is_draft
    is_draft -- yes ---> mark_as_ready
    is_draft -- no ---> reject_label_addition
    mark_as_ready --> remove_other_labels
```


##### What happens when adding `s: needs info`?


```mermaid
---
title: add the needs info label
---
flowchart LR

%% vertices

    trigger([label added])
    remove_other_labels([remove other\n state labels])

%% edges

    trigger --> remove_other_labels
```

##### What happens when adding a state label to an issue?

```mermaid
---
title: add a state label to an issue
---
flowchart LR

%% vertices

    trigger([label added])
    reject_label_addition([reject\n label\n addition])
    nothing([do nothing])
    is_needs_info{is label\n 's: needs info'?}

%% edges

    trigger --> is_needs_info
    is_needs_info -- yes --->  nothing
    is_needs_info -- no --->  reject_label_addition
```

##### What happens when removing a state label from a PR?

```mermaid
---
title: remove a state label
---
flowchart LR

%% vertices

    trigger([label removed])
    nothing([do nothing])
    reject_label_removal([reject\n label\n removal])
    is_needs_info{is label\n 's: needs info'?}

%% edges

    trigger --> is_needs_info
    is_needs_info -- yes --->  nothing
    is_needs_info -- no --->  reject_label_removal
```

Nothing happens when a state label is removed from an issue.



##### What happens when adding a priority label?

```mermaid
---
title: add a priority label
---
flowchart LR

%% vertices

    trigger([label added])
    remove_other_labels([remove other\n priority labels])

%% edges

    trigger --> remove_other_labels
```

##### What happens when removing a priority label?

```mermaid
---
title: remove a priority label
---
flowchart LR

%% vertices

    trigger([label removed])
    reject_label_removal([reject\n label\n removal])

%% edges

    trigger --> reject_label_removal
```



### 📝 Checklist

<!-- Put an `x` in all the boxes that apply. -->
<!-- If your change requires a documentation PR, please link it
appropriately -->
<!-- If you're unsure about any of these, don't hesitate to ask. We're
here to help! -->

- [x] I have made sure that the title is self-explanatory and the
description concisely explains the PR.
- [x] I have linked an issue or discussion.
- [ ] I have created tests covering the changes.
- [ ] I have updated the documentation accordingly.

### ⌛ Dependencies
<!-- List all open pull requests that this PR logically depends on -->
<!--
- #xyz: short description why this is a dependency
- #abc: ...
-->
    
URL: #35172
Reported by: Sebastian Oehms
Reviewer(s): Kwankyu Lee, Sebastian Oehms, Tobias Diez