linters

Stream: lean4

[Yury G. Kudryashov]

Hi, where can I read about (a) builtin linters; (b) std4 linters? What is the difference between two approaches? I want to forward-port some missing linters from mathlib3 and add new ones, and I need docs and/or examples to do that.

[Yury G. Kudryashov]

@Mario Carneiro :up:?

[Mario Carneiro]

@Yury G. Kudryashov

The mathlib linters from lean 3 were ported to what are now the std linters. These run at the end of processing a file or the whole library, using #lint or in a separate stage in CI. They see all declarations in the environment, so they are good for things where even autogenerated definitions need to be linted, but they don't have access to the original syntax so they can't detect things like using the wrong tactics to do something, or bad formatting. These linters are disabled using @[nolint foo] or the nolints.json file.

The lean core linters are new in lean 4, and they trigger immediately after parsing each command. As a result they are better for giving "live feedback", but they are only given the syntax of the command, which means it can be difficult to even determine what things in the environment correspond to it. The elaboration info tree is available however, so these are well suited to linters that want to remark on syntactic things like use of deprecated definitions, unreachable tactics, or unused variables, and the results appear immediately in the editor. These lints are disabled using set_option linter.foo false before the command.

All unported linters are of the std linter kind, because that was the only kind we had in lean 3. But it's possible that they can be reimagined as lean core linters. (We also need better names for both kinds of linters, because neither one really subsumes the other and it's confusing to call them the same.)

[Yury G. Kudryashov]

Is there any documentation for people who want to write these linters (of either kind), or should I look at the source of existing linters and learn from there?

[Mario Carneiro]

there is nothing I am aware of. The linter APIs themselves are fairly simple, but you will want to copy other linters anyway to see the techniques for doing useful things from them

[Mario Carneiro]

example of a std linter: src#Std.Tactic.Lint.defLemma

[Yury G. Kudryashov]

Thank you! I'll start porting the fintype/decidable/encodable/... linter and ask more questions here tomorrow.

[Emilie (Shad Amethyst)]

I would love to see some of the knowledge one can get from analyzing the existing linters to be put down into text somewhere, so it can become less of an arcane art

[Yury G. Kudryashov]

How do I run a specific linter on a specific declaration?

[Yury G. Kudryashov]

Another question: given a docs#Lean.Expr of the form .forallE name type body info, how do I check if body uses this variable?

[Mario Carneiro]

If you want to run a linter on a declaration using the metaprogramming API it looks like this:

import Std
def foo : Nat := 1
#eval Option.isSome <$> Std.Tactic.Lint.docBlame.test ``foo

[Mario Carneiro]

If your expression has no loose bvars (which is generally an invariant for expressions in MetaM) then you can use !body.hasLooseBVars to check if the forall is dependent (or call isArrow which does both this and the forallE match)

[Yury G. Kudryashov]

And what's the right way to descend inside an expr to maintain the "no loose bvars" invariant?

[Mario Carneiro]

either instantiate body with an expression of type type if you have one, or instantiate it with a fresh mvar of that type, or use withLocalDecl to create a fvar of the type and instantiate body with that

[Mario Carneiro]

using instantiate1

[Yury G. Kudryashov]

#xy: I need Lean 4 version of docs3#get_pi_binders_nondep for the linter.

[Yury G. Kudryashov]

I'll try.

[Mario Carneiro]

I would suggest modeling that function after src#Lean.Meta.forallTelescope

[Mario Carneiro]

in particular, it needs to pass its return variables in continuation passing style because the local variables have to exist in an extended context

[Mario Carneiro]

in fact, you might even just do this by calling forallTelescope and postprocessing the returned Array Expr into the desired form

[Mario Carneiro]

and then you don't have to worry about the instantiating and local variable creation

[Yury G. Kudryashov]

AFAICS, forallTelescope won't allow me to use isArrow

[Kyle Miller]

Maybe you could take a look at docs#Lean.Meta.getFunInfo, which processes dependencies between arguments

[Yury G. Kudryashov]

I'll have a look

[Yury G. Kudryashov]

Thanks!

[James Gallicchio]

Maybe would be a good chapter for the metaprogramming book

[James Gallicchio]

(linters, as a topic)

[Yury G. Kudryashov]

You may want to do too many things in a linter...

[Yury G. Kudryashov]

BTW, where can I read about for loops in Lean 4?

[Adam Topaz]

https://lean-lang.org/papers/do.pdf ?

[Adam Topaz]

or are you looking for the docs#ForIn class?

[Yury G. Kudryashov]

Thank you for both links! It looks like I need neither of them right now but I'll read them tomorrow or on Monday.

[Yury G. Kudryashov]

How do I check if a given Expr is of the form ∀ _ _ _, Decidable _?

[Kyle Miller]

Use forallTelescopeReducing (reducing is for handling DecidableRel and such, do forallTelescope if you don't want that), and then for the expr e that it passes to the continuation, do e.isAppOfArity ``Decidable 2

[Yury G. Kudryashov]

I'm using t.getForallBody.isAppOf

[Kyle Miller]

Ok, that's fine -- equivalent to using forallTelescope, but faster since it doesn't instantiate anything, which you don't need here if you're just checking for Decidable.

[Yury G. Kudryashov]

First draft: branch#YK-dec-lint

[Yury G. Kudryashov]

Heavily based on docs#Std.Tactic.Lint.impossibleInstance

[Yury G. Kudryashov]

I know that it doesn't auto ignore decls in Decidable. yet.

[Kyle Miller]

Three comments:

• Rather than (← inferType (← mkConstWithLevelParams declName)) you can do (← getConstInfo declName).type like before
• Rather than if !... then you can use unless ... do
• I'm not sure they ever appear in the wild, but to deal with optParams and such you can do t.cleanupAnnotations.getForallBody.isAppOf

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I'll wait for the CI, then fix the issues.

[Yury G. Kudryashov]

While I'm fixing issues found by this linter, I would appreciate hints for writing a more advanced linter that also catches definitions that assume [Decidable _], then use it for proofs only.

[Mario Carneiro]

I think that would just be asserting that the [Decidable _] binder is nondependent in the theorem's type

[Yury G. Kudryashov]

I meant telling

def ex1 [DecidableEq α] (x y : α) : Nat : if x = y then 0 else 1

from

def ex1 [DecidableEq α] (x y : α) (p : α → α → Prop) (hp : x = y → p x y) (hp' : x ≠ y → p x y) : {n : Nat // p x y} :=
  ⟨1, if h : x = y then hp h else hp' h⟩

[Yury G. Kudryashov]

(of course, IRL p will depend on n)

[Yury G. Kudryashov]

The current implementation does what mathlib3 version did (minus ignoring Decidable.* and Encodable.* for now) but while looking at lint errors, I found some definitions that use decidability for proofs only.

[Mario Carneiro]

hm, I'll take a look at that tomorrow

[Yury G. Kudryashov]

BTW, how do I ask if the definition is computable?

[Kyle Miller]

I haven't tested it, but something you could do is take the body and erase all the proofs with something like

def eraseProofs (e : Expr) : MetaM Expr :=
  Meta.transform e
    (pre := fun e => do
      if (← Meta.isProof e) then
        return .done (← mkSyntheticSorry (← inferType e))
      else
        return .continue)

and then check whether the fvars for the Decidable instances are present.

For interfacing the forallTelescope with the declaration value to get the body, you can use docs#Lean.Expr.beta rather than mkAppN

Expr.beta is to make sure the fvars actually get sunk into the expression. This erasure idea though doesn't detect whether there's some have/let outside the proof that's only used within the proof. I guess for this the transform could also do zeta reduction if that's something you want to handle?

[Yury G. Kudryashov]

IMHO, noncomputable definitions should be treated like theorems: there is no reason to assume [Decidable] if you're not using it in the type and you aren't going to create a computable definition.

[Yury G. Kudryashov]

@Kyle Miller Thanks, I'll test it tomorrow.

[Mario Carneiro]

I'm not sure I agree with that; you can still compute definitions using Decidable using rfl / by decide even if they are noncomputable

[Yury G. Kudryashov]

Let's talk about some specific definition tomorrow. I'm going to bed soon.

[Eric Wieser]

Sometimes you have a structure with multiple fields, and even though one field is non-computable, you want the other one to be defeq to some other computable construction

[Eric Wieser]

The one I feel strongly about is Finsupp.single, which really ought to be defeq to Pi.single (but due to the classical decidable stuff in finsupp it currently isn't)

[Kevin Buzzard]

This could also be solved with nonconstructive finsupps, right?

[Yury G. Kudryashov]

I suggest the following: once I fix all theorems, I run the linter on noncomputable defs, get a list of matches, then we'll discuss whether it's better to enable it on noncomputable defs and add nolints or disable it.

[Kyle Miller]

Another linter idea: find cases of letI or haveI that occur inside proofs, since they could be replaced by let or have, and they're almost certainly accidentally from the port, or from people thinking that the I still stands for "instance" (like from Lean 3) rather than "inline" (which is now what it is in Lean 4).

The condition can't just be "in a proof". Maybe if the expected type at the letI or haveI is a Prop?

This would have to be done in consultation with the InfoTrees, since letI and haveI are not present in the elaborated expression.

[Mario Carneiro]

Kyle Miller said:

Another linter idea: find cases of letI or haveI that occur inside proofs, since they could be replaced by let or have, and they're almost certainly accidentally from the port, or from people thinking that the I still stands for "instance" (like from Lean 3) rather than "inline" (which is now what it is in Lean 4).

Note that it was a conscious decision in mathport to align letI to letI even though the semantics are different, because these are normally used for instances, and it turns out that we generally want them to be inlined too

[Yury G. Kudryashov]

@Kyle Miller I updated the linter so that it should work for defs now (tested on the examples from this thread, awaiting CI).