polyrith fails on simple goal

Stream: mathlib4

[Bolton Bailey]

Working in the web editor, I get an error on the following simple goal:

import Mathlib

example (a b : ℚ) (h : b = 0) : a * b = 0 := by
  polyrith -- polyrith did not find any relevant hypotheses and the goal is not provable by ring

Is there something wrong going on here?

[Richard Copley]

It succeeds if you undo #12258.

[Kim Morrison]

Really? How did you discover that? I don't see anything polyrith relevant there.

[Richard Copley]

Sorry! #12285, the last change to Polyrith.lean

[Richard Copley]

As a workaround, you can say polyrith only when you mean polyrith, and vice versa.
@Cedric Holle, could you have a look?

[Floris van Doorn]

#12754

[Cedric Holle]

Oh, didn't expect that. Added/uncommented some test: https://github.com/leanprover-community/mathlib4/pull/12756.
All the tests from Lean 3 just got copied and commented. This should be changed. I have currently not enough time to do that. I would have more time in ~two months.

[Richard Copley]

They look like Lean 4 (by, not begin/end), but they're mostly commented out for the reasons in the comments: to avoid overwhelming the sagecell server.

[Richard Copley]

It might be ok to uncomment a small number of tests, but it should be considered.

[Cedric Holle]

There are some meta def and setup_tactic_parser, ... uncommented. The changes to by are probably made by a bot.

[Richard Copley]

Oh, thanks.