PANIC at _private.Lean.Meta.Tactic.Grind.Proof

Stream: lean4

[Chris Henson]

I am not sure how to minimize this, because it appears to be a transient panic that I have only seen once in CI. This run has a panic

error: Cslib/Foundations/Data/FinFun.lean:123:67: <GoalM action default value>
info: Cslib/Foundations/Data/FinFun.lean:119:0: PANIC at _private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkCongrProof Lean.Meta.Tactic.Grind.Proof:259:6: assertion violation: rhs.getAppNumArgs == numArgs

that did not replicate on rerunning the job.

[Ruben Van de Velde]

Sounds similar to this one: https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/mathlib.20bors.20notifications/near/564213013

[Kim Morrison]

Thanks for the reports. I can't reproduce yet, but we're thinking about it!

[Jovan Gerbscheid]

Re-posting this grind panic here as it is another instance of the bug discussed in this thread. This one also appeared in Mathlib.Analysis.ODE.PicardLindelof, just like the one posted by Ruben Van de Velde.