breaking the linter

Stream: general

[Kevin Buzzard]

import tactic

constants A B C : Type

@[simp] lemma A_eq_B : A = B := sorry
@[simp] lemma B_eq_A : B = A := sorry
#lint -- excessive memory consumption detected at 'vm'

Perhaps this is not relevant because the code is clearly not production-ready? Not sure. I was just trying to knock up a simple example of the simp linter spotting a problem.

[Kevin Buzzard]

Oh but this hangs it too so maybe there is a problem.

import tactic

def A := ℕ
def B := ℕ

@[simp] lemma A_eq_B : A = B := rfl
@[simp] lemma B_eq_A : B = A := rfl
#lint

[Kevin Buzzard]

Should I open an issue? I am still getting the hang of issues.

[Bryan Gin-ge Chen]

cc: @Gabriel Ebner, who wrote the simp linters.

[Gabriel Ebner]

It is expected that this will cause the linter to fail, because B is not in simp-normal form. (You can simplify it as B = A = B = A = ...)

[Gabriel Ebner]

The excessive memory consumption error is not intended, but I'm not sure if there's an easy way to catch it from the Lean side.

[Kevin Buzzard]

Just to be clear -- the linter hangs lean rather than fails gracefully

[Gabriel Ebner]

Yes, I understand. It is not intentional, but I'm not sure if it's easy to detect. I believe we already have a timeout in there. But feel free to open issue.