Fun "regression" in `ring_nf` (not an actual regression)

Stream: metaprogramming / tactics

[Geoffrey Irving]

Here's a fun issue I just hit during the lean/mathlib upgrade:

I was using ring_nf to close the goal:

2 ^ (62 + -2 ^ 63) = 2 ^ (62 - 2 ^ 63)

where the outer powers are zpow. Before upgrading, this worked fine, as norm_num didn't understand zpow. But now it hangs forever, since norm_num does understand zpow and tries to do the full evaluation. :)

The fix is just to use apply congr_arg₂ _ rfl first, and it's very reasonable that this now fails, but I thought it was worth reporting for amusement value.

[David Renshaw]

I'm surprised that it doesn't hit a timeout.

[Geoffrey Irving]

It’s doing single clock ticks that take ages.

[David Renshaw]

Perhaps we should add logic that bails early if the result is obviously going to be too big (like, requiring more bits than are possible to represent in memory).