[Merged by Bors] - feat(Shake): output clarifications#9996
[Merged by Bors] - feat(Shake): output clarifications#9996Vierkantor wants to merge 2 commits intomasterfrom
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.
grunweg
left a comment
There was a problem hiding this comment.
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.
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.
@Vierkantor, when you have a moment, do you want to make this change and then merge?
There was a problem hiding this comment.
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: |
| -- 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.
| 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.
That's a good idea! Let me make a follow-up PR.
There was a problem hiding this comment.
Actually don't worry about it, I've incorporated this into #9751
A new user running
lake exe shake --fixwill 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.