Zulip Chat Archive
Stream: mathlib4
Topic: linter crash
Yury G. Kudryashov (Mar 06 2023 at 09:07):
Linter crashes, e.g., here: https://github.com/leanprover-community/mathlib4/actions/runs/4341078127/jobs/7580248717
But the job is marked as success anyway.
Yury G. Kudryashov (Mar 06 2023 at 09:10):
It started with !4#2534
Yury G. Kudryashov (Mar 06 2023 at 09:10):
@Joël Riou @Johan Commelin
Kevin Buzzard (Mar 06 2023 at 10:01):
So now is the time to get in any PRs currently being held up by the simpNF linter being picky? [edit: thought not]
Oliver Nash (Mar 07 2023 at 16:42):
I believe this issue is ongoing. Do we have a plan to address it?
Scott Morrison (Mar 07 2023 at 23:05):
!4#2704 is a temporary fix: it avoids generating the PANIC in the first place. We should merge this while we sort out the underlying issue.
Scott Morrison (Mar 07 2023 at 23:48):
I've put a stand-alone repro for this PANIC at lean4#2140.
Scott Morrison (Mar 07 2023 at 23:49):
It is surely not completely minimised, but it seems to be a local minimum, starting from the original code where this appeared.
Scott Morrison (Mar 08 2023 at 00:17):
!4#2705 ensures that panics during linting fail CI.
Last updated: Dec 20 2023 at 11:08 UTC