CI failure in Lint Mathlib

Stream: mathlib4

[Nailin Guan]

Do anyone know what is causing this failure in #28682?
图片.png
This also happened in my other PRs.

[Bryan Gin-ge Chen]

We added a tracing option to the linter (see #mathlib4 > slow linting step CI? @ 💬 ); the error should hopefully be fixed if you merge master.

[Nailin Guan]

Maybe a bit unrelated, but why domy changes totally about ring theory cause this CI failure?
图片.png
Does this imply master is having some trouble? This is really wierd as another PR adding more things isn't failing......

[Bryan Gin-ge Chen]

Instead of a screenshot, can you link to the page? I think you should be able to expand the error on red line 1316 there by clicking on it, and it may give some more details about the error.

[Nailin Guan]

Sorry, here is the link https://github.com/leanprover-community/mathlib4/actions/runs/20740181980/job/59545265202?pr=32316

[Bryan Gin-ge Chen]

Huh, there's a panic in grind: https://github.com/leanprover-community/mathlib4/actions/runs/20740181980/job/59545265202?pr=32316#step:22:1321

I haven't seen this before:

  info: stderr:
  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

  backtrace:
  /home/lean/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/../lib/lean/libleanshared.so(+0x9b24f4e) [0x75343eac9f4e]
  /home/lean/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x1c) [0x75343eaca3dc]
... ( very long backtrace omitted )

[Nailin Guan]

If you refer to #32081 it has no problem anymore...

[Chris Henson]

This panic has been reported previously and is transient.