From 0b107a5d52f97e2e3ea25212b4e1a6fe88bff701 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Tue, 15 Sep 2026 19:39:11 +0200
Subject: [PATCH 1/2] ci: cancel superseded PR runs of Lean Action CI

Add a concurrency group keyed on workflow and ref. On PR refs a new push
cancels the in-flight run. On main and nightly-testing runs queue instead,
since report_failures_nightly-testing.yml consumes every completed run.
---
 .github/workflows/lean_action_ci.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 95bc25bd1..33a2e3e54 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -9,6 +9,11 @@ on:
   merge_group:
   workflow_dispatch:
 
+# Cancel superseded runs on PR branches, but never on main or nightly-testing.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.ref != 'refs/heads/main' && github.ref != 'refs/heads/nightly-testing' }}
+
 jobs:
   ci-checks:
     runs-on: ubuntu-latest

From 29b08cfb1be555d41029586895b925fef3749b35 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Wed, 16 Sep 2026 17:49:31 +0200
Subject: [PATCH 2/2] ci: use a unique concurrency group instead of conditional
 cancel-in-progress

This copies what Mathlib does.
---
 .github/workflows/lean_action_ci.yml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 33a2e3e54..af9ebc99f 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -9,10 +9,12 @@ on:
   merge_group:
   workflow_dispatch:
 
-# Cancel superseded runs on PR branches, but never on main or nightly-testing.
+# Label each run; only the latest run carrying a given label is kept. Pushes to
+# main and nightly-testing get the run id in their label, making it unique, so
+# those runs are never cancelled.
 concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: ${{ github.ref != 'refs/heads/main' && github.ref != 'refs/heads/nightly-testing' }}
+  group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/nightly-testing') && github.run_id) || '' }}
+  cancel-in-progress: true
 
 jobs:
   ci-checks: