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
f2833c2c deleted 22 .idr files under a 'feat: add' message — 4 still untracked #210
Commit f2833c2c, titled "feat: add ECHIDNA validation modules" and authored by Test, deleted 149 files, 22 of them .idr, while its message claims only to add modules.
Five were later restored to the working tree but never re-added to git. Verified against
pristine origin/main today:
Four remain untracked. They are imported by modules that are tracked, so a clean checkout cannot
build — and the module-not-found error is masked by an earlier parse failure, which is why this
was not noticed: the build dies before it gets far enough to complain about the missing file.
Proposed detector — this class is mechanically checkable
For every module named in an .ipkg, and every module transitively imported by one, assert the
source file is present in HEAD.
Cheap, exact, and it would have caught this at the commit that caused it. Nothing in the current
31 workflows checks it. A commit whose message says "add" while its diff deletes 149 files is
also a reviewable signal in its own right.
Activity
fix(idris2): cure seven build blockers — build goes VOID → RED, front…