fix: Lean CI — remove redundant SilverSightFormal build (lake build handled by lean-action)

This commit is contained in:
allaun 2026-06-30 06:45:03 -05:00
parent 1149f0f41b
commit 7dfd05255a

View file

@ -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)