Updating infotrees in linters

Stream: lean4

[Eric Wieser]

In this code, it looks like runLinters discards any updates the linter makes to the infotrees.

Is this a deliberate choice? My impression is that this means it's not possible for a linter to add a tryThis suggestion.

[Damiano Testa]

I don't know if it is deliberate, but I was under the impression that linter were indeed not able to provide Try this suggestions.

[Eric Wieser]

I think replacing

-modify fun s => { savedState with messages := s.messages }
+modify fun s => { savedState with messages := s.messages, infoState := s.infoState }

would fix that

[Damiano Testa]

That would be highly desirable, in my opinion!

[Damiano Testa]

Would that also fix the #guard_msgs not silencing (some) linters? Or is that an independent issue?

[Thomas Murrills]

I think it would be great to let linters modify infotrees somehow, though I wonder if we would want some sort of opt-in on the linter’s end. Or maybe just saying “remember to wrap your linters in (e.g.) withoutModifyingInfoTrees if you don’t want them to modify infotrees” is enough?

[Thomas Murrills]

(Also, for completeness, I’ll link this earlier related thread: #general > code actions in linters)

[Kim Morrison]

I think this would be okay, and the payoff is pretty good. Can we RFC?

[Eric Wieser]

I don't have a good feeling for Thomas' worry above, as I don't really know which actions create new infotrees. I guess the danger is that you end up duplicating hovers somehow?

[Eric Wieser]

I tried this out:

--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -215,7 +215,7 @@ def runLinters (stx : Syntax) : CommandE
             catch ex =>
               logException ex
             finally
-              modify fun s => { savedState with messages := s.messages }
+              modify fun s => { savedState with messages := s.messages, infoState := s.infoState, traceState := s.traceState }

 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule

and can confirm it makes "try this" work

[Eric Wieser]

It also leads to a lot of PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:52:21: unexpected context-free info tree nodes while building lean itself

[Eric Wieser]

The cause is that withSetOptionIn creates a contextless info tree node

[Eric Wieser]

Or perhaps that runLinters is called without an enclosing withInfoTreeContext

[Eric Wieser]

lean4#4363 is the RFC