PA021 ProofDrift: detector matches sorry/oops in Isabelle comment text (false positives) #43

Bug

panic-attack assail's PA021 ProofDrift detector counts the words sorry and oops inside Isabelle \<open>...\<close> and @{text ...} comment blocks, producing false-positive findings on files whose docstrings talk about the keywords (e.g. headers asserting 'zero sorry').

Evidence

In the 2026-05-26 estate sweep, all 4 tropical-resource-typing findings were comment-text matches:

• Tropical_Kleene.thy:663 — All proofs are complete — zero @{text sorry}. — detector counted this as 1 sorry.
• Tropical_Ordinal.thy:15 — with \<open>oops\<close> are the ones we want ECHIDNA to evaluate — detector counted this as 1 oops.
• Tropical_Matrices_Clean.thy:24 — All proofs are complete — zero @{text sorry}. — detector counted this as 1 sorry.
• Tropical_CNO.thy:29 — All sorry placeholders have been closed. — detector counted this as 1 sorry.

grep -nE '\bsorry\b' confirms each file has the keyword only inside comment text, never as a proof tactic.

Fix sketch

PA021's Isabelle detector should skip:

• \<open>...\<close> text blocks
• @{text ...} antiquotations
• text \<open>...\<close> declarations
• (* ... *) Standard ML comment blocks (used in older .thy files)
• Lines after section\<open> / subsection\<open> until matching close

Comparable Agda/Coq/Idris detectors should be re-audited for the same blind spot.

Refs #32 (estate sweep tracker).