[Lean Squad] feat(ci): improve lean-proofs.yml — skip guard and lake update step

[github-actions]

Summary

🔬 Lean Squad — Task 9 (CI Automation), run 2026-04-26.

This PR improves the lean-proofs.yml CI workflow with two practical fixes for the current state of the Lean FV project.

---

Changes

1. Skip guard when no .lean files exist

Added a "Check for Lean source files" step that counts .lean files in FVSquad/. All subsequent heavy steps (elan install, Lean version, cache, lake update, lake build) are now conditional on lean_count != '0'.

Why: Until the first Lean spec is committed, the old workflow would unconditionally trigger a full Mathlib download (~GB of data) on every PR touching formal-verification/lean/**. The skip guard avoids this wasted work while the project is still in the informal-spec phase.

2. Explicit lake update step before lake build

Added a "Resolve Lean dependencies" step that runs lake update before lake build.

Why: Without a committed lake-manifest.json, lake build would either fail or silently run lake update internally. An explicit step makes the dependency-fetch visible, enables better error messages, and ensures the manifest is always generated before the build step runs.

3. Extended cache key to include lean-toolchain

Added lean-toolchain to the cache key hash:

key: lean-$\{\{ runner.os }}-$\{\{ hashFiles('formal-verification/lean/lean-toolchain', 'formal-verification/lean/lakefile.toml', 'formal-verification/lean/lake-manifest.json') }}

Why: If the Lean toolchain version changes, the old elan install is stale. Including the toolchain file invalidates the cache automatically.

4. Create formal-verification/lean/FVSquad/ directory

Added .gitkeep so the directory referenced by lakefile.toml's [[lean_lib]] declaration exists in the repo. This is required by the find command in the skip guard and avoids a missing-path warning from Lake.

---

Verification

• Task 3 (writing .lean files) remains blocked: elan download is blocked by the network firewall in this CI runner environment.
• This PR only touches the CI workflow and directory structure — no Lean source changes.
• Per the hard requirement, no .lean files are committed without a verified lake build.

---

🔬 This PR was created automatically by the Lean Squad FV agent. See workflow run.

---

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 24944826514 -n agent -D /tmp/agent-24944826514

# Create a new branch
git checkout -b lean-squad/task9-ci-2026-04-26-d356b01c58aad2ce main

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

# Push the branch and create the pull request
git push origin lean-squad/task9-ci-2026-04-26-d356b01c58aad2ce
gh pr create --title '[Lean Squad] feat(ci): improve lean-proofs.yml — skip guard and lake update step' --base main --head lean-squad/task9-ci-2026-04-26-d356b01c58aad2ce --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.