[Lean Squad] feat(ci): Task 9 — skip guard + FVSquad scaffold for lean-proofs workflow

[github-actions]

🔬 Lean Squad — Task 9: CI Automation

Summary

Improves lean-proofs.yml with a skip guard and scaffolds the FVSquad/ source directory.

Changes

.github/workflows/lean-proofs.yml — skip guard

Added a Check for Lean source files step that counts .lean files in formal-verification/lean/FVSquad/. All subsequent steps (Install elan, Add elan to PATH, Show Lean version, Cache, Build Lean proofs) are gated on lean_file_count != '0'.

Why: lake build was failing (or would fail) when no .lean source files exist. The skip guard lets the workflow succeed immediately with a clear message until the first Lean target (Phase 3) is committed.

No .lean source files found in FVSquad/ — lake build will be skipped.

This eliminates the class of CI failures reported in issues #7820, #7825, #7843.

formal-verification/lean/FVSquad/README.md — directory scaffold

Creates the FVSquad/ directory with a README documenting:

• Planned .lean targets and their current phases
• The skip-guard behaviour

Verification

The elan v4.2.1 sha256 used in the workflow (4e717523217af592fa2d7b9c479410a31816c065d66ccbf0c2149337cfec0f5c) was independently verified this run against the live release asset.

Task 3 Status

Task 3 (Lean 4 formal spec) remains blocked: the runner sandbox prevents execution of arbitrary binaries (including elan-init). Per the hard requirement, no .lean files are committed without a verified lake build. The skip guard in this PR ensures CI does not fail in the meantime.

---

🔬 Generated by Lean Squad (run #24971730371)

---

Warning

Protected Files — Push Permission Denied

This was originally intended as a pull request, but the patch modifies protected files. A human must create the pull request manually.

Protected files

• .github/workflows/lean-proofs.yml

The push was rejected because GitHub Actions does not have workflows permission to push these changes, and is never allowed to make such changes, or other authorization being used does not have this permission.

Create the pull request manually

# Download the patch from the workflow run
gh run download 24971730371 -n agent -D /tmp/agent-24971730371

# Create a new branch
git checkout -b lean-squad/task9-ci-improvements-2026-04-27-b90542277d8dc525 main

# Apply the patch (--3way handles cross-repo patches)
git am --3way /tmp/agent-24971730371/aw-lean-squad-task9-ci-improvements-2026-04-27.patch

# Push the branch and create the pull request
git push origin lean-squad/task9-ci-improvements-2026-04-27-b90542277d8dc525
gh pr create --title '[Lean Squad] feat(ci): Task 9 — skip guard + FVSquad scaffold for lean-proofs workflow' --base main --head lean-squad/task9-ci-improvements-2026-04-27-b90542277d8dc525 --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.