From f763867d5cb2714560c71c4fb2c258d7fbd27b76 Mon Sep 17 00:00:00 2001
From: justincasher <justinchadwickasher@gmail.com>
Date: Sat, 9 May 2026 11:00:17 -0700
Subject: [PATCH] ci: switch Lean CI trigger from paths-ignore to a paths
 allowlist
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

paths-ignore was too permissive: any change outside python/, *.md, or
LICENSE would trigger a full Lean build, including unrelated workflow
files (e.g. python_ci.yml). Flip to an allowlist of files that can
actually affect the Lean build:

- '**/*.lean'
- 'lakefile.toml'
- 'lean-toolchain'
- 'lake-manifest.json'
- '.github/workflows/lean_action_ci.yml'

Anything else — python/, docs, LICENSE, .gitignore, other workflows —
is now skipped automatically without needing to enumerate it.
---
 .github/workflows/lean_action_ci.yml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 8a878729d8..66d052123f 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -4,17 +4,21 @@ on:
   push:
     branches:
       - main
-    paths-ignore:
-      - 'python/**'
-      - '**/*.md'
-      - 'LICENSE'
+    paths:
+      - '**/*.lean'
+      - 'lakefile.toml'
+      - 'lean-toolchain'
+      - 'lake-manifest.json'
+      - '.github/workflows/lean_action_ci.yml'
   pull_request:
     branches:
       - main
-    paths-ignore:
-      - 'python/**'
-      - '**/*.md'
-      - 'LICENSE'
+    paths:
+      - '**/*.lean'
+      - 'lakefile.toml'
+      - 'lean-toolchain'
+      - 'lake-manifest.json'
+      - '.github/workflows/lean_action_ci.yml'
   workflow_dispatch:
 
 # Cancel superseded runs on the same branch / PR.