Skip to content

ci(verification): fix actionlint SC2086 in lean-build zero-sorry audit#193

Merged
stevenobiajulu merged 1 commit into
mainfrom
fix/actionlint-lean-build-sc2086
May 11, 2026
Merged

ci(verification): fix actionlint SC2086 in lean-build zero-sorry audit#193
stevenobiajulu merged 1 commit into
mainfrom
fix/actionlint-lean-build-sc2086

Conversation

@stevenobiajulu
Copy link
Copy Markdown
Member

Summary

Fixes the actionlint CI check that has been failing since PR #164 merged.

The zero-sorry audit step in .github/workflows/lean-build.yml assembled a list of .lean files into a string variable and then passed it unquoted to grep, relying on shell word-splitting:

files=$(find LeanSpike -name '*.lean' ! -name 'Spec.lean')
files="LeanSpike.lean $files"
if grep -nw "sorry" $files; then    # SC2086

shellcheck/SC2086 flags this — a real footgun if any future filename contains whitespace. actionlint propagated that as a job failure on every push touching the workflow.

Switched to the NUL-delimited pipeline:

if find LeanSpike.lean LeanSpike -name '*.lean' ! -name 'Spec.lean' -print0 \
     | xargs -0 grep -nwH "sorry"; then

Same future-proof glob over all LeanSpike modules except Spec.lean, but correct under any filename.

Test plan

  • actionlint .github/workflows/lean-build.yml exits clean locally
  • Positive case: current zero-sorry repo state → audit exits 1 (audit passes — no forbidden sorries found)
  • Negative case: synthetic sorry injected into a non-Spec module → audit exits 0 with file:line:match printed (audit fails as intended)
  • actionlint CI check passes on this PR

Workflow trigger paths include .github/workflows/lean-build.yml itself, so the lean-build job will also re-run on this PR.

The audit step assembled a file list into a string variable and then
passed it unquoted to grep, relying on word-splitting. shellcheck/SC2086
flagged the unquoted expansion (real footgun if any filename ever
contained whitespace), and actionlint failed on every push as a result.

Switch to `find -print0 | xargs -0 grep -nwH "sorry"` — same
future-proof glob over all LeanSpike modules minus Spec.lean, but
NUL-delimited so the audit is correct under any filename.

Verified locally:
- actionlint clean on the workflow file
- positive case: zero-sorry repo state → audit exits 1 (passes)
- negative case: synthetic sorry in non-Spec module → audit exits 0 (fails)
@vercel
Copy link
Copy Markdown

vercel Bot commented May 11, 2026

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
site Ready Ready Preview, Comment May 11, 2026 4:46pm

Request Review

@stevenobiajulu stevenobiajulu enabled auto-merge (squash) May 11, 2026 16:46
@github-actions github-actions Bot added the ci label May 11, 2026
@stevenobiajulu stevenobiajulu merged commit 54b9dfd into main May 11, 2026
23 checks passed
@codecov
Copy link
Copy Markdown

codecov Bot commented May 11, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@stevenobiajulu
Copy link
Copy Markdown
Member Author

✅ Post-merge smoke passed

Merged: 54b9dfdfed2c2060eb6321505c46370bddeb6de0
Built from: main @ 54b9dfdfed2c2060eb6321505c46370bddeb6de0
Smoke: actionlint + zero-sorry audit positive/negative cases

Steps

  • actionlint .github/workflows/lean-build.yml — clean (the SC2086 that was failing CI is gone)
  • ✅ Positive case: real repo state → audit exits 1 (zero sorries in non-Spec, audit passes)
  • Spec.lean sorry count = 2 (matches the audit expectation)
  • ✅ Negative case: injected synthetic sorry in a non-Spec module → audit exits 0 with file:line:match printed (audit fails as intended)

CI on the merge commit (54b9dfd): 16 success / 1 skipped / 0 failuresactionlint is green again, matching the goal of this fix.

Log: /tmp/automerge-smoke-193-1778518946.log (local).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant