## Stream: general

### Topic: linter

#### Sebastien Gouezel (Nov 08 2019 at 07:56):

I am just compiling the latest mathlib. I got an error

\mathlib\scripts\mk_nolint.lean:8:0: error: invalid import: allKK[2K
could not resolve import: all


#### Sebastien Gouezel (Nov 08 2019 at 08:00):

Never mind, I should just make src.

#### Rob Lewis (Nov 08 2019 at 09:14):

Edit - never mind, I misread this, sorry.

(deleted)

#### Sebastien Gouezel (Dec 06 2019 at 18:25):

#1786 has just been merged, and it contains the following line:

instance fintype.compact_space [fintype α] : compact_space α


I thought that the linter was supposed to ask for a reduced priority on this kind of instance. Has it been deactivated?

#### Floris van Doorn (Dec 06 2019 at 19:15):

I think the instance checker is not yet one of the active linters:
https://github.com/leanprover-community/mathlib/blob/827e78b1638868734de786baac70b5d3f1d5118e/scripts/mk_nolint.lean#L28
https://github.com/leanprover-community/mathlib/blob/740168bf22c86e2d83b98e069b85ac7360dbba8c/scripts/mk_all.sh#L42

#### Floris van Doorn (Dec 06 2019 at 19:15):

(not sure which of these lists is the relevant one, or whether it is necessary that those two lists are the same at all time)

#### Rob Lewis (Dec 06 2019 at 19:28):

The second is the relevant one, and it's most important that the second is a subset of the first. It should be safe to add the priority check back to CI now. With Floris' PRs, I guess almost all of mathlib is passing now. So there should be very few changes to nolints.txt, or none if we update the remaining failures.

#### Sebastien Gouezel (Dec 06 2019 at 19:48):

I vote for enabling it, as this is really a useful check.

#### Rob Lewis (Dec 06 2019 at 21:36):

#1787 passed. Luckily the fintype.compact_space instance was the only bad one that snuck in.

#### Oliver Nash (Dec 26 2019 at 13:28):

I recently learned that it can be dangerous to have a class with more explicit parameters than one which it is extending: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/typeclass.20problems/near/184192445

#### Oliver Nash (Dec 26 2019 at 13:29):

I'm not quite sure exactly what the rule would be, but I wonder if this is the sort of thing we could have the linter warn about?

#### Floris van Doorn (Jan 06 2020 at 14:18):

Yes, this is definitely something we can have the linter warn about. I think the rule is
"There cannot be a local constant in one of the (type-class) hypotheses that does not occur in the conclusion (and cannot be inferred from the type of the local constants in the conclusion)."
I'm not sure if the parenthetical is necessary.

There are instances which violate this rule, coe_trans comes to mind:

coe_trans : Π {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [_inst_1 : has_coe a b] [_inst_2 : has_coe_t b c], has_coe_t a c


However, instances like those do raise issues:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/remove.20all.20instances.20with.20variable.20domain

#### Mario Carneiro (Jan 06 2020 at 22:18):

outparams are also excepted from this rule

#### Kevin Buzzard (Mar 22 2020 at 23:54):

I have a small laptop and failing eyesight (meaning that when I can't find my specs I have to turn font size up), and I really like the rule which says that lines in mathlib are supposed to be at most 100 characters long. Not every line in mathlib has this property though. I would be very happy if this became a hard and fast rule. Can we lint for it, or is this considered to just be some sort of guideline and most people don't actually care about it?

#### Yury G. Kudryashov (Mar 23 2020 at 02:37):

I have a PR with a slightly longer line that I can't (or at least don't want to) break. It is a markdown link to a section of a Wikipedia page.

#### Yury G. Kudryashov (Mar 23 2020 at 02:38):

Currently 2258 lines in *.lean files have >100 characters.

#### Yury G. Kudryashov (Mar 23 2020 at 02:39):

And another ~600 have =100 characters. So people try to follow this rule.

#### Johan Commelin (Mar 23 2020 at 08:00):

One problem with such a linter is that it's not so easy to write a nolint attribute for it. (I think.)

#### Rob Lewis (Mar 23 2020 at 10:17):

This kind of thing doesn't fit in the current linter framework. The linter has no access to the source code.

#### Rob Lewis (Mar 23 2020 at 10:17):

If someone wants to implement a syntactic linter, I won't complain, but it's basically a separate tool from the existing linters.

#### Johan Commelin (Mar 24 2020 at 20:17):

I was running #lint on a new file, and noticed that it did not complain about the missing copyright header and missing module docstring. Is that because those are more "syntactic" issues? Or could the linter do that as well?

#### Gabriel Ebner (Mar 24 2020 at 20:18):

I think the missing module docstring should be lintable. But the copyright header is out of scope.

#### Gabriel Ebner (Mar 24 2020 at 20:18):

But even the module docstring linter doesn't fit into the current framework at all.

#### Simon Hudon (Mar 24 2020 at 20:25):

I've been working on a small change to the tactic parser so that we can specify linters for specific tactics. It looks something like:

set_option trace.lint.tactic true

namespace tactic.linter

meta def simp (p : parse cur_pos) ... := do
simp ...,
gs <- get_goals,
unless (gs.empty) \$ advice p "non-terminal use of simp"

end tactic.linter

lemma my_proof : something :=
begin
-- more stuff
end


#### Simon Hudon (Mar 24 2020 at 20:27):

does that sound useful?

#### Simon Hudon (Mar 24 2020 at 20:28):

This particular advice could be bolted in the core library but if we want to define linter in mathlib (or other libraries) for tactics defined in core, that would seems useful

#### Kevin Buzzard (Mar 24 2020 at 20:29):

Not directly related to the linter, but my students often use non-terminal simps and it would be nice if such a thing generated some kind of warning. I believe that simp, ring is used in mathlib though.

#### Mario Carneiro (Mar 24 2020 at 21:58):

Yeah, unfortunately a nonterminal simp lint is going to generate a lot of false positives

#### Simon Hudon (Mar 24 2020 at 21:59):

Yeah, this is not pitch for this specific rule so much as a way of building such rules

#### Mario Carneiro (Mar 24 2020 at 21:59):

However, if we can make constructions like this, does this mean we can get access to the tactic scripts now? I know that there were other lints that needed that

#### Simon Hudon (Mar 24 2020 at 22:00):

Yes, I think so. I'm looking into using that right now

#### Mario Carneiro (Mar 24 2020 at 22:02):

it would be great if we could store these into olean files for later analysis

#### Mario Carneiro (Mar 24 2020 at 22:04):

I'm trying to remember what the use cases were... I think the imported files lint has false positives if a file is imported for its tactics

#### Simon Hudon (Mar 24 2020 at 22:05):

Yeah, I remember. I'm not touching the olean file right now but I see where the tactic is parsed. It seems to be discarded quickly

#### Mario Carneiro (Mar 24 2020 at 22:07):

maybe create an auxiliary def with the tactic that was used? Could be a bit noisy, but there aren't very many other ways to store data

#### Mario Carneiro (Mar 24 2020 at 22:09):

maybe it only produces the def if some set_option is set

I like that idea

#### Simon Hudon (Mar 24 2020 at 23:59):

The switch and the extra definion

#### Kenny Lau (Nov 19 2020 at 14:25):

Currently it takes 64 minutes to lint mathlib on PRs even if you only change one file. Can we make this faster perhaps by caching?

#### Johan Commelin (Nov 19 2020 at 14:32):

I think that especially for the simp linter, this is hard. And I expect that's also one of the slower linters.

#### Eric Wieser (Nov 19 2020 at 15:56):

Can we run the linters in parallel with each other (in separate processes or even jobs) rather than sequentially?

#### Gabriel Ebner (Nov 19 2020 at 16:01):

I tried to parallelize the linters (i.e. running one task per linter):
https://github.com/leanprover-community/mathlib/compare/parlint

#### Gabriel Ebner (Nov 19 2020 at 16:01):

This doesn't help much because (at least at the time) the simp linter takes 95% of the runtime.

#### Gabriel Ebner (Nov 19 2020 at 16:02):

You can't run each declaration in a task either, because that's expensive (see comment in PR ^^).

#### Gabriel Ebner (Nov 19 2020 at 16:02):

I think the best approach would be to split the declaration list into chunks and then run each chunk in a task.

#### Rob Lewis (Nov 19 2020 at 16:13):

I tried this (naively) at some points and it led to segfaults. Never investigated beyond that though, it's quite possible I was doing something wrong.

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

Note: in Lean 3, VM functions executed in tasks need to copy their whole closure and return values twice.

Additional note: Lean segfaults when copying lists that are more than few hundred elements long.

The branch I've linked to ^^ solves this by using buffer instead.

#### Sebastian Ullrich (Nov 19 2020 at 17:30):

Gabriel Ebner said:

Note: in Lean 3, VM functions executed in tasks need to copy their whole closure and return values twice.

Additional note: Lean segfaults when copying lists that are more than few hundred elements long.

Solved in Lean 4, it now prints a proper stack overflow error message

#### Sebastian Ullrich (Nov 19 2020 at 17:30):

Oh, it also doesn't copy closures to begin with...

Last updated: May 15 2021 at 23:13 UTC