From cd8280700df80971344253bfdda52031f0ec4771 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Wed, 28 Jan 2026 14:13:48 +1100 Subject: [PATCH] fix: create PR releases even when test suite fails (#12202) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes an issue where PR releases were not created when the test suite failed, even though the build artifacts were available. The workflow now runs whenever a PR's CI completes, regardless of success/failure, and relies on the artifact verification step to ensure the necessary build artifacts exist before proceeding. This allows developers to get PR toolchains and test against Mathlib even when the Lean test suite has failures, as long as the build jobs succeeded. 🤖 Prepared with Claude Code Co-authored-by: Claude --- .github/workflows/pr-release.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index dfcfef266f..4dd93fd04a 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -20,7 +20,9 @@ on: jobs: on-success: runs-on: ubuntu-latest - if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4' + # Run even if CI fails, as long as build artifacts are available + # The "Verify release artifacts exist" step will fail if necessary artifacts are missing + if: github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4' steps: - name: Retrieve information about the original workflow uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin