From a106ea053fec080a50204b0ad6dadc69bc3f0937 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Thu, 20 Nov 2025 16:19:02 +1100 Subject: [PATCH] test: split grind_lint.lean into 7 smaller files for faster CI (#11271) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR splits the single grind_lint.lean test (50+ seconds) into 7 separate files that each run in under 7 seconds: - grind_lint_list.lean (5.7s): List namespace with exceptions - grind_lint_array.lean (4.6s): Array namespace - grind_lint_bitvec.lean (3.9s): BitVec namespace with exceptions - grind_lint_std_hashmap.lean (6.8s): Std hash map/set namespaces - grind_lint_std_treemap.lean (~6s): Std tree map/set namespaces - grind_lint_std_misc.lean (~5s): Std.Do, Std.Range, Std.Tactic - grind_lint_misc.lean (5.5s): All other non-Lean namespaces Each file maintains complete namespace coverage and preserves all existing exceptions. The split enables better CI parallelization and faster feedback. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude --- tests/lean/run/grind_lint_array.lean | 7 +++++ tests/lean/run/grind_lint_bitvec.lean | 17 +++++++++++ tests/lean/run/grind_lint_list.lean | 33 ++++++++++++++++++++++ tests/lean/run/grind_lint_misc.lean | 7 +++++ tests/lean/run/grind_lint_std_hashmap.lean | 7 +++++ tests/lean/run/grind_lint_std_misc.lean | 7 +++++ tests/lean/run/grind_lint_std_treemap.lean | 7 +++++ 7 files changed, 85 insertions(+) create mode 100644 tests/lean/run/grind_lint_array.lean create mode 100644 tests/lean/run/grind_lint_bitvec.lean create mode 100644 tests/lean/run/grind_lint_list.lean create mode 100644 tests/lean/run/grind_lint_misc.lean create mode 100644 tests/lean/run/grind_lint_std_hashmap.lean create mode 100644 tests/lean/run/grind_lint_std_misc.lean create mode 100644 tests/lean/run/grind_lint_std_treemap.lean diff --git a/tests/lean/run/grind_lint_array.lean b/tests/lean/run/grind_lint_array.lean new file mode 100644 index 0000000000..c62a6a7e4c --- /dev/null +++ b/tests/lean/run/grind_lint_array.lean @@ -0,0 +1,7 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! Check Array namespace: -/ + +#guard_msgs in +#grind_lint check (min := 20) in Array diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean new file mode 100644 index 0000000000..09f7bba9d7 --- /dev/null +++ b/tests/lean/run/grind_lint_bitvec.lean @@ -0,0 +1,17 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! `BitVec` exceptions -/ + +-- `BitVec.msb_replicate` is reasonable at 25. +#guard_msgs in +#grind_lint inspect (min := 30) BitVec.msb_replicate + +-- `BitVec.msb_signExtend` is reasonable at 22. +#guard_msgs in +#grind_lint inspect (min := 25) BitVec.msb_signExtend + +/-! Check BitVec namespace: -/ + +#guard_msgs in +#grind_lint check (min := 20) in BitVec diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean new file mode 100644 index 0000000000..453929ded5 --- /dev/null +++ b/tests/lean/run/grind_lint_list.lean @@ -0,0 +1,33 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! `List` exceptions -/ + +-- TODO: Not sure what to do here, see https://lean-fro.zulipchat.com/#narrow/channel/503415-grind/topic/.60.23grind_lint.60.20command/near/556730710 +-- #grind_lint inspect List.getLast?_concat +#grind_lint skip List.getLast?_concat + +-- TODO: We should consider changing the grind annotation for `List.getElem?_eq_none` +-- so it only fires if we've already proved the hypothesis holds. (i.e. the new gadget) +-- Other than that, everything looks sane here: +-- #grind_lint inspect List.getLast?_pmap +#grind_lint skip List.getLast?_pmap + +-- TODO: `List.Sublist.eq_of_length` should probably only fire when we've already proved the hypotheses. + +-- `List.replicate_sublist_iff` is reasonable at 30. +#guard_msgs in +#grind_lint inspect (min := 30) List.replicate_sublist_iff + +-- `List.Sublist.append` is reasonable at 25. +#guard_msgs in +#grind_lint inspect (min := 25) List.Sublist.append + +-- `List.Sublist.middle` is reasonable at 25. +#guard_msgs in +#grind_lint inspect (min := 25) List.Sublist.middle + +/-! Check List namespace: -/ + +#guard_msgs in +#grind_lint check (min := 20) in List diff --git a/tests/lean/run/grind_lint_misc.lean b/tests/lean/run/grind_lint_misc.lean new file mode 100644 index 0000000000..a48d4dbde4 --- /dev/null +++ b/tests/lean/run/grind_lint_misc.lean @@ -0,0 +1,7 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! Check miscellaneous namespaces: -/ + +#guard_msgs in +#grind_lint check (min := 20) in Acc Attr Bool Clause Const Decidable DefaultClause DHashMap Equiv ExceptT ExtDHashMap Fin Int Internal InvImage Lex LRAT Nat NormalizePattern OldCollector Option OptionT Perm Prod PSigma Quot Quotient Rat Raw ReaderT ReflCmp Setoid StateT Subrelation Subtype Sum Tactic Task Vector WellFounded diff --git a/tests/lean/run/grind_lint_std_hashmap.lean b/tests/lean/run/grind_lint_std_hashmap.lean new file mode 100644 index 0000000000..e822103088 --- /dev/null +++ b/tests/lean/run/grind_lint_std_hashmap.lean @@ -0,0 +1,7 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! Check Std hash/tree map/set namespaces: -/ + +#guard_msgs in +#grind_lint check (min := 20) in Std.DHashMap Std.HashMap Std.HashSet Std.ExtDHashMap Std.ExtHashMap Std.ExtHashSet diff --git a/tests/lean/run/grind_lint_std_misc.lean b/tests/lean/run/grind_lint_std_misc.lean new file mode 100644 index 0000000000..5b998f6b37 --- /dev/null +++ b/tests/lean/run/grind_lint_std_misc.lean @@ -0,0 +1,7 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! Check remaining Std sub-namespaces: -/ + +#guard_msgs in +#grind_lint check (min := 20) in Std.Do Std.Range Std.Tactic diff --git a/tests/lean/run/grind_lint_std_treemap.lean b/tests/lean/run/grind_lint_std_treemap.lean new file mode 100644 index 0000000000..285d212eb9 --- /dev/null +++ b/tests/lean/run/grind_lint_std_treemap.lean @@ -0,0 +1,7 @@ +import Std +import Lean.Elab.Tactic.Grind.Lint + +/-! Check Std tree map/set namespaces: -/ + +#guard_msgs in +#grind_lint check (min := 20) in Std.DTreeMap Std.TreeMap Std.TreeSet Std.ExtDTreeMap Std.ExtTreeMap Std.ExtTreeSet