hanging linter

Stream: general

[Kevin Buzzard]

This hangs the linter for me:

import tactic

open_locale big_operators

/-- define a constant c to break the linter -/
def c : ℚ := ∑ n in finset.range 1320, (-1)^(n + 1) / n

#lint -- hangs

It's something to do with the 1320 -- if I change the number to something like 20, it takes ten seconds on my machine but it terminates. Unfortunately the number is not some random number, this is coming from an IMO question (it's approximately 2/3 of 1979).

[Reid Barton]

If there isn't a fix immediately forthcoming, then to get unstuck you should create an issue on github and add a @[nolint] here (hopefully this is enough to make the timeout go away) with a comment referring to the issue.

[Kevin Buzzard]

thanks

[Gabriel Ebner]

Slightly minimized:

import tactic

open_locale big_operators

/-- define a constant c to break the linter -/
def c : ℚ := ∑ n in finset.range 1320, (-1)^(n + 1) / n

#eval tactic.is_class `(c) -- hangs

[Gabriel Ebner]

MWE (slightly different error though):

def c : ℕ := if 999999999 < 9999999999 then 0 else 1

#eval tactic.is_class `(c)

[Kevin Buzzard]

I tried @[nolint] and it asked which linter. I was in the process of finding out the names of the linters when my laptop battery gave up the ghost because I'd hammered it with the linting :-) Do you know which linter I should avoid?

[Gabriel Ebner]

lean#502

[Gabriel Ebner]

@[nolint fails_quickly]

[Kevin Buzzard]

Lol thanks