feat: show diffs when #guard_msgs fails #3912
Conversation
david-christiansen
requested review from
kmill
and removed request for
kim-em and
digama0
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
|
@nomeata you've asked about this a few times. Does this PR cover your use case? |
|
Sounds great to me, but maybe should be 3 separate PRs (diffs, subarrays, guard_msgs)? No objection if someone else wants to merge as is. |
|
(Sorry, wrong button!) |
| @@ -99,6 +99,10 @@ v4.8.0 (development in progress) | |||
| and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking. | |||
| PR [#3883](https://github.com/leanprover/lean4/pull/3883). | |||
|
|
|||
| * The `#guard_msgs` command now supports showing a diff between the expected and actual outputs. This feature is currently | |||
| disabled by default, but can be enabled with `set_option guard_msgs.diff true`. Depending on user feedback, this option | |||
| may default to `true` in a future version of Lean. | |||
There was a problem hiding this comment.
Why not on by default? If it's off I expect few people will ever benefit from it, simply because they don't know about it.
We can still turn it off by default if it's not well received.
There was a problem hiding this comment.
For both this and in expected type mismatch messages, I think both views are useful, but I don't think a set_option is the best way to surface it to users, a toggle button in the info view would be better. (The issue with only having the diff view is that it can make it difficult to see what either the before or after expression is because the two are mixed together. Also, if there is very little similarity between the two I think the diff formatting is not so helpful.)
There was a problem hiding this comment.
I agree that an infoview toggle would be better, but it's not achievable in the time I have right now. Any creative ideas to implement something nicer on the Lean side?
Another reason to have it off by default right now is that the practicality of something like this is hard to assess in the abstract, or with contrived examples. I plan to have it on for a couple of months, and I'm sure a bunch of little papercuts will surface that I can fix.
I'm already expecting that I'll want a threshold of similarity that triggers the diff rendering (e.g. if less than X% of lines are edited, show a diff, otherwise don't), but I'd rather base that kind of thing on real experience by myself and others.
The plan is to make it on by default once it makes people happy enough, but I'd rather have the experiment be opt-in to start with.
|
OK, I think this is both good enough to be useful and unlikely to get substantially better in the next little while - I'll merge, then dogfood for a while to make it really nice and polished |
Adds the ability to show a diff when
guard_msgsfails, using the histogram diff algorithm pioneered in jgit. This algorithm tends to produce more user-friendly diffs, but it can be quadratic in the worst case. Empirically, the quadratic case of this implementation doesn't seem to be slow enough to matter for messages smaller than hundreds of megabytes, but if it's ever a problem, we can mitigate it the same way jgit does by falling back to Myers diff.See lean/run/guard_msgs.lean in the tests directory for some examples of its output.