Merge main into nightly-testing

test/lint_unreachableTactic.lean

@@ -1,5 +1,12 @@
 import Batteries.Linter.UnreachableTactic
 
+-- The warning generated by `linter.unreachableTactic` is not suppressed by `#guard_msgs`,
+-- because the linter is run on `#guard_msgs` itself. This is a known issue, see
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60
+-- We jump through an extra hoop here to silence the warning.
+set_option linter.unreachableTactic false in
+#guard_msgs(drop warning) in
+set_option linter.unreachableTactic true in
 /--
 warning: this tactic is never executed
 note: this linter can be disabled with `set_option linter.unreachableTactic false`