From 87418d60728d0d7a0e80749cce7dfe673fe5dd0f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 18 Apr 2026 10:51:00 +1000 Subject: [PATCH] feat: add tech debt counter for disabled varHead simp warnings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a counter for `set_option warning.simp.varHead false` occurrences to the weekly tech debt report. The `warning.simp.varHead` option silences a warning introduced in Lean about simp lemmas whose LHS has a metavariable as its head. Places where this warning is silenced are tech debt we want to track over time. Prompted by discussion on https://github.com/leanprover-community/mathlib4-nightly-testing/pull/209 which adds several `set_option warning.simp.varHead false in` uses. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.7 (1M context) --- scripts/reporting/technical-debt-metrics.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/reporting/technical-debt-metrics.sh b/scripts/reporting/technical-debt-metrics.sh index 29933d3..33a1e86 100755 --- a/scripts/reporting/technical-debt-metrics.sh +++ b/scripts/reporting/technical-debt-metrics.sh @@ -132,6 +132,8 @@ doubleDeprecs="$(git grep -A2 -- "set_option linter.deprecated false" -- ":^Math printf '%s|disabled deprecation lints\n' "$(( deprecs - doubleDeprecs ))" +printf '%s|%s\n' "$({ git grep -c 'set_option warning.simp.varHead false' -- Mathlib Archive Counterexamples || true; } | awk -F: 'BEGIN{s=0}{s+=$2} END{print s}')" "disabled varHead simp warnings" + printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nolint entries" printf '%s|%s\n' "$(grep -c 'tacticDocs' scripts/nolints.json)" "undocumented tactics" # We count the number of large files, making sure to avoid counting the test file `MathlibTest/Lint.lean`.