Skip to content

Commit be1171e

Browse files
committed
chore(hypatia): exempt formal/Rows.v from the V-lang ban (per-file matcher)
.hypatia-ignore matches `${rule}:${path}` as fixed-string whole-line equality (grep -qxF), not a glob — so each formal/*.v needs its own two lines. The new Rows.v scaffold is a Coq proof script like its 16 siblings; add the same vlang_detected + banned_language_file exemptions so a sweep cannot mis-flag it as V-lang. (Rows.v stays un-wired from _CoqProject — the exemption is about the file in the tree, independent of the build graph.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa
1 parent d66bfab commit be1171e

1 file changed

Lines changed: 7 additions & 0 deletions

File tree

.hypatia-ignore

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,3 +75,10 @@ cicd_rules/vlang_detected:formal/F5_RenderFaithful.v
7575
cicd_rules/banned_language_file:formal/F5_RenderFaithful.v
7676
cicd_rules/vlang_detected:formal/RealWasm.v
7777
cicd_rules/banned_language_file:formal/RealWasm.v
78+
# Rows.v — record-row soundness scaffold (Wave-W0). Authored without a Coq
79+
# toolchain, so it is UNVERIFIED and deliberately NOT in formal/_CoqProject;
80+
# it is still a Coq proof script in the tree and must be exempted from the
81+
# V-lang ban like its siblings (the ignore matcher is fixed-string per-file,
82+
# not a glob, so a new .v needs its own lines).
83+
cicd_rules/vlang_detected:formal/Rows.v
84+
cicd_rules/banned_language_file:formal/Rows.v

0 commit comments

Comments
 (0)