Can linters see tactic proofs?

Stream: metaprogramming / tactics

[Jason Rute]

My understanding is that Linters are triggered after each declaration. I want to know if they can see the syntax of the declaration and not only the expressions. In particular, can a linter see the tactic proofs. I'm imagining a case, for example, where a linter is set up to gather online proof data about a declaration right after it is declared (for example each goalstate-tactic pair in the proof). This data can be used for online AI tactics that occur later in the same file.

[Damiano Testa]

I think that linters can see the syntax, but, depending on the information that you want them to extract from the syntax, you may have to essentially re-parse the file.

Here is an example of a "linter" that prints the current file as many times as there are declarations in the file.

import Std.Tactic.Lint.Frontend

open Lean (getEnv) in
/-- This linter shows that linters have access to the each file containing
a declaration. -/
@[std_linter] def Std.Tactic.Lint.printFile : Linter where
  noErrorsFound := "No declarations in this file."
  errorsFound := "Declarations found."
  test declName := do
    if "Std.Tactic.Lint.printFile".isPrefixOf declName.toString then
      return none
    let currModule := (← getEnv).mainModule
    let fPath := Lean.modToFilePath "" currModule "lean"
    let fPath := ⟨fPath.toString.drop 1⟩
    return m!"\n\n{← IO.FS.readFile fPath}"

theorem printThisFile : True := .intro

#lint

Since the linter runs inside the MetaM monad, it can do quite a bit of processing from the .lean file.

[Jason Rute]

So I think you are saying is that I can do this if I relates the Lean file from the beginning. Obviously not ideal, but good to know.

[Jason Rute]

And just to give another example which I think the Mathlib folks would be more interested in, if say one wanted to make a linter to find non-terminal simp tactics would it have to work like this (regarding the whole file)?

[Jason Rute]

Also, I guess there is also the issue that a Lean file might not be saved.

[Damiano Testa]

Yes, I would say that Expr information is "readily avaiable", since linters have access to the environment. However, they also have access to whatever text you actually typed in the file and then they can run anything that MetaM can run. So, I think that very little is out of scope.

[Damiano Testa]

Right, if the file is not saved, then what I wrote will not "see" it. I do not know if you can see unsaved changes to a file.

[Damiano Testa]

Jason Rute said:

And just to give another example which I think the Mathlib folks would be more interested in, if say one wanted to make a linter to find non-terminal simp tactics would it have to work like this (regarding the whole file)?

I think that Scott has a repository that computes a lot of information from files, more than you find just in the environment. I think that his tools give access to Syntax trees, but I have not explored it in detail.

[Jason Rute]

Yes, I’ve seen it, but I’m brainstorming ways to use online information found in the same file.

[Damiano Testa]

This is the repository that I was thinking of: https://github.com/semorrison/lean-training-data

[Damiano Testa]

I think that this is the usual "only X can parse X": you can probably get away with extracting some information quickly, but to "do it right", I suspect that you have no alternative but to parse the file.

[Jason Rute]

Actually docs#Lean.MonadFileMap.getFileMap is interesting. It seems to access the current file in the editor even with unsaved changes.

[Damiano Testa]

That link does not work for me and suggests using https://leanprover-community.github.io/mathlib4_docs/Lean/Data/Position.html#Lean.MonadFileMap.getFileMap instead.

[Jason Rute]

Fixed

[Mario Carneiro]

@Jason Rute There are two linter frameworks, and now that they are both in lean core I can't call them "lean linters" and "std/mathlib linters" anymore, the replacement terminology is "syntax linter" and "environment linter". The linter framework used in @Damiano Testa 's code block is an environment linter, and these do not have access to the syntax of the declaration. If you need the syntax you should be using a syntax linter, these are run automatically after each definition and report warnings directly on the definition (like the unused variables linter), and they are given access to both the syntax of the current command, as well as the info trees generated during elaboration of the command, so you can also cross reference the syntax to any generated expressions.

[Jason Rute]

@Mario Carneiro Thanks for the clarification! Do you have an example of a syntax linter, especially one that looks at tactics if it is available?

[Mario Carneiro]

https://github.com/leanprover/std4/blob/main/Std/Linter/UnreachableTactic.lean

[Jason Rute]

@Mario Carneiro Can CommandElabM access MetaM at the position of a tactic to see the state before the tactic was run? I can use the info tree to find the goal mvid but I don’t know if I can run getType on that mvId.

[Adam Topaz]

if you have access to the infotree, you can traverse the tree and obtain the info context as well as the tactic info associated to that particular tactic invocation, then run MetaM using those.

[Adam Topaz]

docs#Lean.Elab.TacticInfo has both the mvar context before and after the tactic

[Adam Topaz]

docs#Lean.Elab.ContextInfo.runMetaM should also be useful here.

[Jason Rute]

Thanks! I think I figured it out.

[Jason Rute]

I also found Scott’s https://github.com/semorrison/lean-training-data helpful.

[Adam Topaz]

yeah I learned a lot from that repo :) Specifically my answer is essentially based on https://github.com/semorrison/lean-training-data/blob/e0072c48bd926e51c49a8d77667395d57fe076c0/TrainingData/InfoTree/TacticInvocation/Basic.lean#L34