Zulip Chat Archive

Stream: general

Topic: linter


view this post on Zulip 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
could not resolve import: all

view this post on Zulip Sebastien Gouezel (Nov 08 2019 at 08:00):

Never mind, I should just make src.

view this post on Zulip Rob Lewis (Nov 08 2019 at 09:14):

Edit - never mind, I misread this, sorry.

view this post on Zulip Rob Lewis (Nov 08 2019 at 09:14):

(deleted)

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

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

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

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

view this post on Zulip Sebastien Gouezel (Dec 06 2019 at 19:48):

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

view this post on Zulip Rob Lewis (Dec 06 2019 at 21:36):

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

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

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

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

view this post on Zulip Mario Carneiro (Jan 06 2020 at 22:18):

outparams are also excepted from this rule

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

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

view this post on Zulip Yury G. Kudryashov (Mar 23 2020 at 02:38):

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

view this post on Zulip Yury G. Kudryashov (Mar 23 2020 at 02:39):

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

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

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

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

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

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

view this post on Zulip Gabriel Ebner (Mar 24 2020 at 20:18):

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

view this post on Zulip 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
   simp, -- prints advice here
   -- more stuff
end

view this post on Zulip Simon Hudon (Mar 24 2020 at 20:27):

does that sound useful?

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

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 21:58):

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

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

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

view this post on Zulip Simon Hudon (Mar 24 2020 at 22:00):

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 22:02):

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 24 2020 at 22:09):

maybe it only produces the def if some set_option is set

view this post on Zulip Simon Hudon (Mar 24 2020 at 23:58):

I like that idea

view this post on Zulip Simon Hudon (Mar 24 2020 at 23:59):

The switch and the extra definion

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

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

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

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

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

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

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

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

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

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

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