You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Two checks red on main for reasons unrelated to any PR: lint-workflows (SPDX must be line 1) and estate-audit (sorry-prose false positives, e2e TODOs) #105
1. lint-workflows (workflow-linter.yml) — ERROR: … missing SPDX header for every file under .github/workflows/, "Add '# SPDX-License-Identifier: MPL-2.0' as first line". The files have the header, on line 2; line 1 is # This workflow is managed by gh actions-lock. The linter requires line 1. Either the linter accepts the header within the first N lines, or actions-lock emits its banner after the SPDX line.
2. estate-audit (main-estate-audit.yml, cicd-suite check.sh) — two things:
"Untracked debt markers": tests/e2e.sh:72,81,88 carry template # TODO: lines (mint scaffold, never instantiated). Resolve or link as MARKER(#issue).
"Undeclared proof circumventions": the scanner greps sorry and matches the prose/-! ## Axiom audit (sorry-free check) -/ headers in all eight Lean files and the "(sorry-free; …)" sentences in doc comments. The repo's own proof-scan-dangerous recipe is comment-aware for exactly this reason; the estate scanner is not. Options: make the suite comment-aware, or list the eight modules in .cicd-hygiene-allow with the trusted-base count as the error text suggests.
Both symptoms are green on main after #107, so this is closed as completed. For the record, neither was fixed the way the issue proposed:
lint-workflows: the SPDX line is still line 2 in every workflow (line 1 is the gh actions-lock banner). The linter was relaxed instead: .github/workflows/workflow-linter.yml now accepts the SPDX tag anywhere in the leading comment block. Green at 41519571422.
estate-audit: main-estate-audit.yml had the real miss (no permissions: block); it now has one, with SPDX on line 2. tests/e2e.sh has no TODO lines any more. Green at 41519571352. How the "sorry" prose false positive was cleared upstream in the pinned cicd-suite was not checked.
Activity
hyperpolymath commentedon Nov 4, 2026
Both symptoms are green on
mainafter #107, so this is closed as completed. For the record, neither was fixed the way the issue proposed:lint-workflows: the SPDX line is still line 2 in every workflow (line 1 is thegh actions-lockbanner). The linter was relaxed instead:.github/workflows/workflow-linter.ymlnow accepts the SPDX tag anywhere in the leading comment block. Green at 41519571422.estate-audit:main-estate-audit.ymlhad the real miss (nopermissions:block); it now has one, with SPDX on line 2.tests/e2e.shhas no TODO lines any more. Green at 41519571352. How the "sorry" prose false positive was cleared upstream in the pinned cicd-suite was not checked.Generated by Claude Code