From 7dfd05255a38fa42973e5b21601dc88f547e2e09 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 30 Jun 2026 06:45:03 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20Lean=20CI=20=E2=80=94=20remove=20redunda?=
 =?UTF-8?q?nt=20SilverSightFormal=20build=20(lake=20build=20handled=20by?=
 =?UTF-8?q?=20lean-action)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .github/workflows/lean-check.yml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/.github/workflows/lean-check.yml b/.github/workflows/lean-check.yml
index 0c7cbea4..6893938a 100644
--- a/.github/workflows/lean-check.yml
+++ b/.github/workflows/lean-check.yml
@@ -7,10 +7,6 @@ jobs:
       - uses: actions/checkout@v4
       - name: Install Lean
         uses: leanprover/lean-action@v1
-      - name: Build default target
-        run: lake build
-      - name: Build formal library
-        run: lake build SilverSightFormal
       - name: Check for non-TODO sorries
         run: |
           SORRY_COUNT=$(grep -rn "^  sorry$\|^  sorry$\|^sorry$" formal/SilverSight/ Core/ || true | wc -l)