debugging test failure

Stream: mathlib4

[llllvvuu]

It seems I've caused a seemingly unrelated test failure (test/RewriteSearch/Polynomial.lean) in a small PR (specifically, starting from this commit). Does anyone know what it could be? It passes locally for me (lake env lean test/RewriteSearch/Polynomial.lean; I've also tried merging master and re-building). Did I perhaps cause it to timeout on CI?

[Yury G. Kudryashov]

It looks like it finds sub_eq_add_neg while the test expects sub_eq_neg_add. I don't understand how either is expected to succeed.

[Yury G. Kudryashov]

UPD: I see

[Yury G. Kudryashov]

It starts with natDegree_sub, I missed that.

[Yury G. Kudryashov]

So, you've changed something, and it finds a different solution to the same problem now.

[Yury G. Kudryashov]

Last time it changed solution was in #9083. @Scott Morrison Should we have this unstable test at all?

[llllvvuu]

Thanks, that fixed it! Seems related: https://github.com/leanprover-community/mathlib4/issues/9410