Heron linter

Stream: general

[Willem vanhulle]

Hi I just started working on a linting and refactoring tool for Lean. Unfortunately I had to fork Lean4 to get access to context for creating replacements and diagnostics. It’s still early on but I thought was good to announce it already here before I get started on defining lots of rules https://codeberg.org/wvhulle/heron

[Eric Wieser]

I guess https://github.com/leanprover/lean4/compare/master...wvhulle:lean4:master is the patches you had to make in the fork?

[Willem vanhulle]

Yes indeed. But i think there are too many different things at once now. It needs to be split up before reviewing is possible. I’ll do that in the coming weeks after testing the changes for a while.

[Thomas Murrills]

By the way, are you aware of my WIP Skimmer? We overlap on the focus on refactoring, and, as it happens, also on water-bird-inspired naming, down to including an image of the bird in the readme. :)

Am I understanding correctly that the primary goal of Heron is providing an extensible(?) way to

1. conveniently register extensions to certain syntax linters, so that they can...
2. ...provide code actions and command-palette interfaces for modifying or testing code you're looking at

If so, I think we might be going after slightly different niches after all; I'm focusing on extensible library-wide observation and manipulation "all at once" (i.e. on code you're not looking at), and on providing an interactive in-lean DSL for managing the same.

I'd be really curious to hear what changes you needed to make to core and why! You seem to have focused quite a bit on editor integration, which is very cool. I'd expect the core changes to involve allowing linters to add code actions/infotree nodes (though I'm not sure if you worked around this differently), and on editor integration. But I also see some changes to lake whose purpose I can't quite discern.

Note: for my part, I've tried to be careful trying to avoid modifying lean itself in my own work, even though it would help a lot; hence I've spent some time backtracking and switching approaches. Skimmer is technically public here, but disclaimer that I'm very much "working with the garage door open", so to speak; the repo isn't nearly ready for primetime, the code is in a truly frightful state, and the README refers to my previous approach, not the current one, which is being grown on branches other than main.