## Stream: general

### Topic: hanging linter

#### Kevin Buzzard (Nov 17 2020 at 12:11):

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 (Nov 17 2020 at 12:26):

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.

thanks

#### Gabriel Ebner (Nov 17 2020 at 12:56):

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 (Nov 17 2020 at 13:05):

MWE (slightly different error though):

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

#eval tactic.is_class (c)


#### Kevin Buzzard (Nov 17 2020 at 13:14):

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?

lean#502

#### Gabriel Ebner (Nov 17 2020 at 13:15):

@[nolint fails_quickly]

#### Kevin Buzzard (Nov 17 2020 at 14:43):

Lol thanks

Last updated: May 10 2021 at 18:22 UTC