[tools] Fix bug in state comparison - #2000
Merged
Merged
Conversation
maranget
force-pushed
the
fix-mcompare
branch
from
September 14, 2026 12:49
0eb094f to
f2eadb0
Compare
psafont
approved these changes
Sep 14, 2026
psafont
left a comment
psafont
left a comment
Contributor
There was a problem hiding this comment.
Separating the refactorings from the behavioral change, as well as explaining that the exact error was in the commit message would help in reviewing the code.
From what I understood, the issue was that that the diffing was not reducing the problem on the recursive call when the second argument is more than the first one.
| if r < 0 then sts1@diff stss1 (sts2::stss2) | ||
| else if r > 0 then diff stss1 (sts2::stss2) | ||
| if r < 0 then sts1@diff r1 stss2 | ||
| else if r > 0 then diff stss1 r2 |
Contributor
There was a problem hiding this comment.
This is the only change in behaviour I could find, the list passed as second parameter for diff has one fewer element now.
Member
Author
There was a problem hiding this comment.
Hi @psafont, you are correct. Sorry for having hidden the fix.
maranget
force-pushed
the
fix-mcompare
branch
from
September 14, 2026 14:28
f2eadb0 to
592982c
Compare
maranget
commented
Sep 14, 2026
Comment on lines
-422
to
+426
| if r < 0 then sts1@diff stss1 (sts2::stss2) | ||
| else if r > 0 then diff stss1 (sts2::stss2) | ||
| if r < 0 then sts1@diff r1 stss2 | ||
| else if r > 0 then diff stss1 r2 |
Member
Author
There was a problem hiding this comment.
I have updated the commit message.
Very unfortunate error in implementing
the difference of two sorted lists.
The wrong code was in the definition of `do_diff_state`:
```OCaml
let r = cmp_by_env sts1 sts2 in
if r < 0 then sts1@diff stss1 (sts2::stss2)
else if r > 0 then diff stss1 (sts2::stss2)
...
```
Which should have been:
```OCaml
let r = cmp_by_env sts1 sts2 in
if r < 0 then sts1@diff stss1 (sts2::stss2)
else if r > 0 then diff (sts1::stss1) stss2
...
```
maranget
force-pushed
the
fix-mcompare
branch
from
September 14, 2026 14:31
592982c to
090ad08
Compare
Member
Author
|
Merged, thanks @psafont for the quick review. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Very unfortunate error in implementing the difference of two sorted lists, introduced by PR #1970.