request for help with failure in Archive

Stream: mathlib4

[Scott Morrison]

lean4#2790 changes the way some "internal" errors are handled, and it particular makes it "harder to catch" them, so when they occur they will break whatever is going on.

#8056 is the Mathlib adaptation PR.

There are currently several failures of simp or norm_num, all occurring in Archive/, where previously a "max recursion depth" error was being caught, and then the recovery path successfully finished the proof, but now the max recursion depth error is causing a crash.

If anyone is able to look at these, that would be very helpful! A first step might just be to identify where the error is coming from, and/or who used to catch it!

[Eric Wieser]

Does locally increasing the depth help?

[Mauricio Collares]

Not super helpful but: similar to the failure Leo fixed in Lean's testsuite as part of lean4#2790, this seems to be related to simp calling decide (in this case, norm_num is calling simp). I haven't actually checked it but I'm saying this because in #7834 I had to change the same line that's failing tests in Imo1960Q2.lean.

[Scott Morrison]

Eric Wieser said:

Does locally increasing the depth help?

Ah, should have said this: no, increasing the depth only makes it slower, it still fails.

[David Renshaw]

I pushed an ugly workaround for Imo1962Q1: https://github.com/leanprover-community/mathlib4/pull/8056/commits/e2c18145218773d1dd36a85d1ef3c0ccfc8c437a

[David Renshaw]

(and opened some related discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/whnf.20blowup.20in.20Nat.2Edigits/near/399757322 )

[Patrick Massot]

Note that Archive/Imo/Imo1960Q1 is still failing.

[David Renshaw]

"fixed" Imo1960Q1 with the same idea here: https://github.com/leanprover-community/mathlib4/pull/8056/commits/f95d8117507cc9401a046ffd9d49764e2373cd18

[David Renshaw]

This actually makes the proof go much faster than it currently does on master

[David Renshaw]

workaround for BirthdayProblem: https://github.com/leanprover-community/mathlib4/pull/8056/commits/0010b07b87adb9fa5d065e6c1a2b5898729907bf