comment out DeriveTraversable

kim-em · kim-em · commit 0460eb84ed78 · 2025-09-12T09:00:55.000+10:00
diff --git a/Mathlib/Tactic/DeriveTraversable.lean b/Mathlib/Tactic/DeriveTraversable.lean
@@ -8,6 +8,11 @@ import Lean.Elab.Match
 import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
 
+/-
+#adaptation_note nightly-2025-09-11
+
+This is broken on nightly-testing, but unused in Mathlib, so I am commenting it out for now.
+
 /-!
 # Deriving handler for `Traversable` instances
 
@@ -494,3 +499,5 @@ def lawfulTraversableDeriveHandler : DerivingHandler :=
 initialize registerDerivingHandler ``LawfulTraversable lawfulTraversableDeriveHandler
 
 end Mathlib.Deriving.Traversable
+
+-/
diff --git a/MathlibTest/Traversable.lean b/MathlibTest/Traversable.lean
@@ -1,6 +1,11 @@
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Control.Traversable.Instances
 
+/-
+#adaptation_note nightly-2025-09-11
+
+This is broken on nightly-testing, but unused in Mathlib, so I am commenting it out for now.
+
 set_option linter.style.commandStart false
 
 namespace Testing
@@ -85,3 +90,5 @@ example : (ex.run []).2 = [1, 2, 3, 3, 2, 1] := rfl
 end
 
 end Testing
+
+-/
