Run ci for a PR only if it's labeled ci. Added mergify rules

.github/mergify.yml

@@ -0,0 +1,22 @@
+# https://docs.mergify.com/merge-queue/lifecycle/
+# The merge queue tests pull requests against the latest version of the base branch. Therefore, if a new commit is pushed to the base branch, Mergify resets the process and starts over with the updated base branch.
+
+# https://docs.mergify.com/configuration/file-format/
+pull_request_rules:
+  - name: "Automatic queue when CI passes and approved"
+    conditions:
+      # Mergify receives an PR event(`opened``, `reopened`` and etc.), does some actions(`queue` here) if following conditions are all true.
+      - "#approved-reviews-by>=2"
+      - "check-success=tests"
+    actions:
+      queue:
+queue_rules:
+  - name: default
+    queue_conditions:
+      # Mergify receives `queue` or `requeue` command, queues the PR if following conditions are all true.
+      - "#approved-reviews-by>=1"
+      - "check-success=tests"
+    merge_conditions:
+      - "check-success=tests"
+    merge_method: squash
+    update_method: rebase

.github/workflows/tests.yml

@@ -7,16 +7,29 @@ on:
       - 'docs/**'
       - '*.md'
   pull_request:
-    types: [ opened, synchronize, reopened, edited ]
+    types: [ opened, synchronize, reopened, edited, labeled ]
     paths-ignore:
       - 'docs/**'
       - '*.md'
 
 jobs:
   tests:
     name: tests
+    # https://docs.github.com/en/actions/using-jobs/using-conditions-to-control-job-execution
+    # https://github.com/orgs/community/discussions/26261
+    if: ${{ github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'ci') }}
     runs-on: [ "self-hosted", "avx512" ]
     steps:
+    # https://github.com/hmarr/debug-action
+    #- uses: hmarr/debug-action@v2
+
+    - name: Show PR labels
+      run: |
+        echo "Workflow triggered by ${{ github.event_name }}"
+        if [[ ${{ github.event_name }} == 'pull_request' ]]; then
+          echo "PR labels: ${{ join(github.event.pull_request.labels.*.name, ', ') }}"
+        fi
+
     - name: Ensure workspace ownership
       run: echo "chown -R $USER $GITHUB_WORKSPACE" && sudo chown -R $USER $GITHUB_WORKSPACE