[Lean Squad] feat(ci): Task 9 — fix elan SHA256, cache ordering, conditional lake update, proof summary

[github-actions]

Improves lean-proofs.yml with four targeted fixes for correctness and efficiency.

Changes

1. Fix SHA256 verification bug (correctness fix)

The previous workflow hardcoded the SHA256 hash from elan v3.1.0 while downloading v4.2.1. The sha256sum -c step would always fail once .lean files were committed and the build actually ran. The fix: download the .sha256 checksum file from the same GitHub Releases URL and verify against it dynamically. Upgrading elan in the future requires only a version bump, not a hash update.

2. Cache-before-install ordering (performance fix)

Moved the cache restore step to before the elan install step. elan install and lake update are now both gated on cache-hit != 'true', so warm builds (cache hit) skip straight to lake build. Previously the cache was restored after elan was already installed, giving no benefit to the install step.

3. Conditional lake update (correctness fix)

lake update previously ran on every CI run, potentially drifting lake-manifest.json away from the committed state. It now runs only on cache miss (i.e., the first run for a given toolchain/lakefile hash combination).

4. Proof summary step (observability)

After a successful lake build, a Markdown summary is posted to the GitHub Actions step summary showing theorem/lemma count and the number of sorry-bearing lines (stub markers). This gives a quick at-a-glance view of proof progress directly in the CI UI.

---

🔬 Lean Squad — automated formal verification agent
Run: https://github.com/microsoft/testfx/actions/runs/25043800787

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

---

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

# Create a new branch
git checkout -b lean-squad/task9-ci-proof-summary-2026-04-28-c4f8dc642ffc3bc0 main

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

# Push the branch and create the pull request
git push origin lean-squad/task9-ci-proof-summary-2026-04-28-c4f8dc642ffc3bc0
gh pr create --title '[Lean Squad] feat(ci): Task 9 — fix elan SHA256, cache ordering, conditional lake update, proof summary' --base main --head lean-squad/task9-ci-proof-summary-2026-04-28-c4f8dc642ffc3bc0 --repo microsoft/testfx

Generated by 📐 Lean Squad, see workflow run.