Enable "Auto label" for merge-queue actions

[tautschnig]

This will Fix merge-queue CI actions as this is a required CI action, but wasn't being run for jobs entering the queue.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jaisnan]

Thanks!

[celinval]

This workflow will potentially invoke the benchcomp workflow, which I think may require changes as well, since it has code that depends on the event trigger. Can you please double check! Thanks

[tautschnig]

This workflow will potentially invoke the benchcomp workflow, which I think may require changes as well, since it has code that depends on the event trigger. Can you please double check! Thanks

The job for invoking benchcomp workflows is defined as verification-bench in the very same file that this PR touches, so I believe we are actually fine here.

[celinval]

In that workflow, we have this code to extract the commits that will be compared:

kani/.github/workflows/bench.yml

Lines 20 to 30 in 4a92557

	- name: Save push event HEAD and HEAD~ to environment variables
	if: ${{ github.event_name == 'push' }}
	run: |
	echo "NEW_REF=${{ github.event.after}}" | tee -a "$GITHUB_ENV"
	echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV"
	- name: Save pull request HEAD and base to environment variables
	if: ${{ contains(fromJSON('["pull_request", "pull_request_target"]'), github.event_name) }}
	run: |
	echo "OLD_REF=${{ github.event.pull_request.base.sha }}" | tee -a "$GITHUB_ENV"
	echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"

I think in the new case, it won't enter any of these steps, and the commits to be compared will not be defined.

[tautschnig]

In that workflow, we have this code to extract the commits that will be compared:

[...]

Oh, thank you for highlighting this, you are absolutely right. I will fix this, but the way I intend to fix this is by not running this performance check workflow for merge queues at all. My reasons for doing this are:

1. The job is not marked as "Required," so failures will not block the queue from progressing.
2. No one will look at the individual job outcomes when the merging attempt does not fail.
3. We run performance verification upon pushing to main anyway.

[celinval]

In that workflow, we have this code to extract the commits that will be compared:
[...]

Oh, thank you for highlighting this, you are absolutely right. I will fix this, but the way I intend to fix this is by not running this performance check workflow for merge queues at all. My reasons for doing this are:

1. The job is not marked as "Required," so failures will not block the queue from progressing.

2. No one will look at the individual job outcomes when the merging attempt does not fail.

3. We run performance verification upon pushing to `main` anyway.

Sounds good to me!