diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index a43f740a43f1..615a8ff6c0aa 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -1,21 +1,20 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Run performance benchmarks comparing two different Kani versions. +# This workflow takes much longer than other workflows, so we don't run it by default. +# This workflow will run when: +# - Changes are pushed to 'main'. +# - Triggered by another workflow name: Kani Performance Benchmarks on: push: branches: - 'main' - pull_request: - types: - - labeled + workflow_call: jobs: perf-benchcomp: - if: ${{ github.event_name == 'push' - || (github.event_name == 'pull_request' - && github.event.action == 'labeled' - && github.event.label.name == 'Z-BenchCI') - }} runs-on: ubuntu-20.04 steps: - name: Save push event HEAD and HEAD~ to environment variables @@ -25,7 +24,7 @@ jobs: echo "OLD_REF=${{ github.event.before }}" | tee -a "$GITHUB_ENV" - name: Save pull request HEAD and base to environment variables - if: ${{ github.event_name == 'pull_request' }} + 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" diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml new file mode 100644 index 000000000000..d4da80fbe132 --- /dev/null +++ b/.github/workflows/extra_jobs.yml @@ -0,0 +1,49 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Workflow that execute jobs based on the files that were changed or some label configuration. +# +# The first job in this workflow will auto label the PR, while the following jobs will conditionally +# run according to the auto-label result. +# +# This workflow runs on `pull_request_target` because the labeler needs extra write permission. +# Thus, we keep this job minimal, and the only actions used are from the same verified publisher. +# +# Other jobs should not require extra permissions, so be careful when adding new jobs to not propagate write +# permissions. +# +# Note that this also means that the workflow version run is the one currently in `main`, +# not the one from the PR. This is only relevant if a PR is changing this workflow. +# +# See for more details. + +name: Kani Extra +on: pull_request_target + +jobs: + # Keep this job minimal since it requires extra permission + auto-label: + name: Auto Label + permissions: + contents: read + pull-requests: write + outputs: + all-labels: ${{ steps.labeler.outputs.all-labels }} + new-labels: ${{ steps.labeler.outputs.new-labels }} + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v3 + + - name: Label PR + id: labeler + uses: actions/labeler@v4 + with: + dot: true + + verification-bench: + name: Verification Benchmarks + needs: auto-label + permissions: {} + if: contains(needs.auto-label.outputs.all-labels, 'Z-BenchCI') + uses: ./.github/workflows/bench.yml diff --git a/.github/workflows/labeler.yml b/.github/workflows/labeler.yml deleted file mode 100644 index 70f7bf61e36b..000000000000 --- a/.github/workflows/labeler.yml +++ /dev/null @@ -1,30 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -# -# Auto label PRs based on the files that were changed -# -# This PR runs on `pull_request_target` because it needs extra write permission. -# -# Thus, we keep this workflow minimal, and the only action used here is from a -# verified publisher. -# -# See for more details. - -name: Auto Label -on: pull_request_target - -jobs: - auto-label: - permissions: - contents: read - pull-requests: write - runs-on: ubuntu-latest - steps: - - name: Checkout Kani - uses: actions/checkout@v3 - - - name: Label PR - uses: actions/labeler@v4 - with: - dot: true -