Merge branch 'main' into rfc-region-cov

.github/workflows/audit.yml

@@ -7,6 +7,7 @@
 name: Cargo Audit
 on:
   pull_request:
+  merge_group:
   push:
     # Run on changes to branches but not tags.
     branches:

.github/workflows/extra_jobs.yml

@@ -18,7 +18,9 @@
 # See <https://github.com/actions/labeler/issues/121> for more details.
 
 name: Kani Extra
-on: pull_request_target
+on:
+  pull_request_target:
+  merge_group:
 
 jobs:
   # Keep this job minimal since it requires extra permission
@@ -45,5 +47,5 @@ jobs:
     name: Verification Benchmarks
     needs: auto-label
     permissions: {}
-    if: contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI')
+    if: ${{ contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI') && github.event_name != 'merge_group' }}
     uses: ./.github/workflows/bench.yml

.github/workflows/format-check.yml

@@ -3,6 +3,7 @@
 name: Kani Format Check
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.

.github/workflows/kani.yml

@@ -3,6 +3,7 @@
 name: Kani CI
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.

.github/workflows/release.yml

@@ -8,6 +8,7 @@
 name: Release Bundle
 on:
   pull_request:
+  merge_group:
   push:
     branches:
       - 'main'

.github/workflows/toolchain-upgrade.yml

@@ -36,6 +36,7 @@ jobs:
         run: git clean -f
 
       - name: Create Pull Request
+        id: create_pr
         if: ${{ env.next_step == 'create_pr' }}
         uses: peter-evans/create-pull-request@v6
         with:
@@ -47,14 +48,25 @@ jobs:
             Update Rust toolchain from nightly-${{ env.current_toolchain_date }} to
             nightly-${{ env.next_toolchain_date }} without any other source changes.
 
-            This is an automatically generated pull request. If any of the CI checks fail,
-            manual intervention is required. In such a case, review the changes at
-            https://github.com/rust-lang/rust from
-            https://github.com/rust-lang/rust/commit/${{ env.current_toolchain_hash }} up to
-            https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log
-            for this commit range is:
+      - name: Add debugging hints
+        if: ${{ steps.create_pr.outputs.pull-request-number }}
+        uses: actions/github-script@v7
+        with:
+          script: |
+            github.rest.issues.createComment({
+              issue_number: ${{ steps.create_pr.outputs.pull-request-number }},
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              body: `This is an automatically generated pull request. If any of the CI checks fail,
+                manual intervention is required. In such a case, review the changes at
+                https://github.com/rust-lang/rust from
+                https://github.com/rust-lang/rust/commit/${{ env.current_toolchain_hash }} up to
+                https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log
+                for this commit range is:
+
+                ` + process.env.git_log
+            })
 
-            ${{ env.git_log }}
       - name: Create Issue
         if: ${{ env.next_step == 'create_issue' }}
         uses: dacbd/create-issue-action@main

.github/workflows/verify-std-check.yml

@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome