linter

Stream: general

[Sebastien Gouezel]

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

[Sebastien Gouezel]

Never mind, I should just make src.

[Rob Lewis]

Edit - never mind, I misread this, sorry.

[Rob Lewis]

(deleted)

[Sebastien Gouezel]

#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]

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]

(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]

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]

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

[Rob Lewis]

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

[Oliver Nash]

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]

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]

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]

outparams are also excepted from this rule

[Kevin Buzzard]

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]

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]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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]

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

[Gabriel Ebner]

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

[Simon Hudon]

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

[Simon Hudon]

does that sound useful?

[Simon Hudon]

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]

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]

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

[Simon Hudon]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

maybe it only produces the def if some set_option is set

[Simon Hudon]

I like that idea

[Simon Hudon]

The switch and the extra definion

[Kenny Lau]

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]

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

[Eric Wieser]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Rob Lewis]

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]

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]

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]

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