-
Notifications
You must be signed in to change notification settings - Fork 259
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
[Merged by Bors] - feat(Shake): output clarifications #9996
Conversation
A new user running `lake exe shake --fix` will see lots of messages like "add:" "remove:" "fix:" and won't know what to do with it. I think these minor changes to the output will massively clarify what the tool actually wants you to do.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can certainly confirm that the changes make the output much clearer.
Other questions (such as "how will a user find out this exists, or know what it does, or discover the "--fix" flag) can be discussed after this PR.
The command will run in CI and suggest running with the |
Shake/Main.lean
Outdated
|
||
-- Since we throw an error upon encountering issues, we can be sure that everything worked | ||
-- if we reach this point of the script. | ||
println!"All suggestions applied successfully." |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably there should be a special case here in case the edit list is empty, e.g. No edits required.
instead
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Vierkantor, when you have a moment, do you want to make this change and then merge?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since there is the possibility that the edit list is nonempty but nothing gets applied, I ended up counting the number of edits in the edit-apply-loop.
bors d+ |
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
That way we don't say "All edits applied." if there were none
Although the change might have been larger than you might have expected, I'm going to be bold and say: bors merge |
A new user running `lake exe shake --fix` will see lots of messages like "add:" "remove:" "fix:" and won't know what to do with it. I think these minor changes to the output will massively clarify what the tool actually wants you to do.
Pull request successfully merged into master. Build succeeded: |
@@ -407,50 +410,60 @@ def main (args : List String) : IO Unit := do | |||
|
|||
-- Apply the edits to existing files | |||
if !args.fix then return | |||
edits.forM fun mod (remove, add) => do | |||
let count ← edits.foldM (fun count mod (remove, add) => do |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
let count ← edits.foldM (fun count mod (remove, add) => do | |
let count ← edits.foldM (init := 0) fun count mod (remove, add) => do |
I really hate it when the 0
argument is passed 40 lines later
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's a good idea! Let me make a follow-up PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually don't worry about it, I've incorporated this into #9751
A new user running
lake exe shake --fix
will see lots of messages like "add:" "remove:" "fix:" and won't know what to do with it. I think these minor changes to the output will massively clarify what the tool actually wants you to do.