Troubleshooting assertion violation

Stream: general

[Bolton Bailey]

Trying to get this repository to work, I get the following error:

Lean (version 4.0.0-nightly-2023-03-09, commit 0cc9d7a43de7, Release)
PANIC at _private.Lean.Meta.Match.MatchEqs.0.Lean.Meta.Match.SimpH.substRHS Lean.Meta.Match.MatchEqs:167:2: assertion violation: ( __do_lift._@.Lean.Meta.Match.MatchEqs._hyg.2199.0 ).xs.contains rhs

I am not sure what this error means, it looks like there is a error generated by the Lean library, rather than the code in the library I downloaded. Is this right?

[Floris van Doorn]

Yes, the panic occurs at the line assert! (← get).xs.contains rhs, line 167 of Lean.Meta.Match.MatchEqs of the Lean 4 repo.

[Bolton Bailey]

Does this mean a bug report needs to be filed with the library then? (Or perhaps I should upgrade lean and see if that fixes it)?

[Floris van Doorn]

Probably, but it would be helpful to see what piece of code is causing it. Maybe the repo is doing something clearly illegal and the problem is only that you get a panic instead of a nice error message.
It's looks like it's related to making equation lemmas for match expressions.

[Bolton Bailey]

The issue is, it's a big project and I don't know how to locate what part of it is calling this assertion. I guess it's some call to simp? What is SimpH?

[Kim Liesinger]

It seems the error is in MatchingLogic/Proof.lean. It's quite annoying the error message doesn't tell us which declaration or command the PANIC occurred in. You could probably localize it by doing a binary search by moving #exit around in the file in VSCode, however lame that sounds. :-)