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!