-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Linter / Formatter Wishlist #7217
Comments
Hello @BoltonBailey
White spacingHere is a list I collected from comments on a PR a while ago:
|
Non-Terminal SimpThe second to last item in your current list is "Non-terminal simp". My understanding is a terminal See this #6052 (comment) |
@MohanadAhmed A "terminal" simp means a simp at the end of a tactic block. The example in that comment is of a terminal simp. So the linter warning would be for a |
@digama0 Thanks for the correction. I am curios what is your opinion on how feasible is it to make a formatter in Lean code that runs almost instantly (say like javascript or similar in VSCode) ? |
Significant architectural changes are required to make a formatter which runs faster than |
It's [proposed](#7217) that a code formatter remove those automatically, so we might as well remove them as we see them.
I am compiling a list of things we might like our linter / possible future code formatters / reviewdog to detect/correct/comment on. Feel free to add to this list, or augment items with related issues.
Linters
Style Guide Items
:
and:=
and infix operators:
and:=
go before linebreaks.:
,:=
by
is placed on the line prior to the first tactic↦
preferred to=>
(only slightly)λ
disallowed in favor offun
Items not in the style guide which might nevertheless be nice
simp
(calls to simp that do not close the goal) should be replaced withsimp?
output.simp at
andsimp [...]
calls should be linted as well.variables
keyword in the file when possible.Shake
)<-
to←
.rw
/simp only
into one call, when this doesn't affect proof readability.simp
/simp only
withsimp_rw
where possible/not too verbose, so that readers can use their cursor to inspect the effect of each step.rw
with unspecified arguments, this makes the proof harder to read.variable {α : Type*}
at the top of the file, and then the same declaration again below.(∀ i, α i)
or((i : X) -> α i)
according to whether theα i
values areProp
ssimp only
calls don't use unnecessary lemmasalgHom_C
, addkillCompl_C
#11205, this problem caught me up for a while, but was a one-character fix.Formatters
A formatter does not exist yet, but when it does, the above issues should be revisited.
(Thanks to Floris, @MohanadAhmed, Sebastien Gouezel for contributing points)
The text was updated successfully, but these errors were encountered: