[Merged by Bors] - feat: a linter to enforce formatting#24465
[Merged by Bors] - feat: a linter to enforce formatting#24465
Conversation
Found by the linter in #24465. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de> Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
Found by the linter in #24465. Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de> Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
| if L.take 3 == "/--" && M.take 3 == "/--" then | ||
| parallelScanAux as (L.drop 3) (M.drop 3) else |
There was a problem hiding this comment.
If I understand this bit of code right, it's going to check formatting differently between multi-line comments /- -/ and documentation /-- -/. I can't really find a testcase for this, could you at least add a comment explaining the difference here?
There was a problem hiding this comment.
I would describe this slightly differently: I am trying as hard as possible to scan the strings one character at a time. However, the substring -- plays a role different than /--, so there should be some awareness when -- is encountered of whether it was preceded by / or not. This is pre-empted by first looking ahead and checking if the string is /--, in which case we discard 3 characters right away. After that, whenever we find --, we are guaranteed that it was a comment and not a doc-string. And, when we do encounter --, we discard until the following line break.
I'll add this comment to the code as well.
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
I am quite impressed at the way the linter works, the pretty-printer is impressive that it can already do all this formatting, and robustly too.
Some suggestions aimed at explainability of the code, but overall looks good to me!
bors d+
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
adomani
left a comment
adomani
left a comment
There was a problem hiding this comment.
Anne and Michael, thank you so much for your reviews! I accepted all the suggestions and added some comments to the code.
I'll merge master, fix any further issues if necessary and merge!
|
bors merge Finally! 😄 |
|
Pull request successfully merged into master. Build succeeded: |
6 participants
This linter enforces that the hypotheses of every declaration are correctly formatted.
This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.
The default linter option is
false, but the lakefile enforces it to betrue.This means that the linter does not run on
MathlibTest. However, the tests should still be compliant, since the default option wastruein development and the tests were fixed.