Building tests failure

Stream: mathlib4

[Rida Hamadani]

The last CI for #16032 has failed to build test/RewriteSearch/Polynomial.lean, but I've only added new lemmas, without modifying old ones, and they seem to be unrelated to the proof that fails. Why would this happen, and how to fix it?

[Martin Dvořák]

Adding new lemmas can make rewrite_search fail. That said, I didn't look at the PR you mentioned.

[Rida Hamadani]

Yes, that's the tactic that is failing. I've tried excluding the new lemmas from therw_searchbut it is still failing. Are there any solutions to this?

[Kim Morrison]

I pushed a fix to the test.

[Rida Hamadani]

Thank you!