recursive ring

Stream: general

[Patrick Massot]

Is that a bug?

import tactic.ring

example (a b x y : ℤ) :  -x*y*(a+b)^2 + y*(x+y)*a^2 + x*(x+y)*b^2 - (a*y-b*x)^2 = 0:=
begin
  ring,
  ring,
end

[Kenny Lau]

so ring is not idempotent ^^

[Mario Carneiro]

ring has a bug in it currently

[Mario Carneiro]

I think there's an issue for it

[Patrick Massot]

The example in the issue actually works here

[Mario Carneiro]

It's because when ring fails, it tries to rewrite the expression into a "nice" SOP form, and this rewriting causes it to circumvent the bug the second time around

[Sebastian Ullrich]

begin ring, ring, ring, ring, ring, ring, ring, banana_phone end

[Patrick Massot]

I really mean: I copy and paste the example in the github issue and it works here