grunweg
grunweg
Some concrete proposals for moving forward - #29 enables mk_all in the default .yml file - one could similarly add `shake` - text-based linters: blocked on the mathlib PR (which...
Brief status update: - a shake step shouldn't be hard to add - there is a mathlib linter set now - so I would suggest adding that to the lakefile...
Welcome to mathlib and thank you for your contribution! Is your pull request ready for review? Then you can label it `awaiting-review`, so reviewers will look at it :-) (Have...
Feel free to label as ready for review, once you have fixed the build failures.
@eric-wieser If I see correctly, this is off the bors queue. Can you approve again, if you agree with the changes?
#14620 contains a few of these fixes. As discussed with adomani, let's land these fixes as a follow-up, and land the linter now.
It's a syntax linter; it can be found in Mathlib/Tactic/Linter/Lint.lean.
Created #14621 with just the newly added sections/namespaces.
The fixes to the other files have landed; I have merged master. This PR now just contains the linter. I still think the implementation is good. maintainer merge
This looks exciting :tada: So, just to clarify: can I run this on an entire file like #find_home?