Zulip Chat Archive

Stream: general

Topic: hanging linter


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 17 2020 at 12:26):

thanks

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Nov 17 2020 at 13:14):

lean#502

view this post on Zulip Gabriel Ebner (Nov 17 2020 at 13:15):

@[nolint fails_quickly]

view this post on Zulip Kevin Buzzard (Nov 17 2020 at 14:43):

Lol thanks


Last updated: May 10 2021 at 18:22 UTC