feat: better merge algorithm #4910
Merged
Conversation
This file contains 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
aryairani
reviewed
May 3, 2024
aryairani
reviewed
May 3, 2024
| Tip: Use `merge /topic1 /main` to merge your work back into | ||
| the main branch. | ||
| Tip: To merge your work back into the main branch, first | ||
| `switch /main` then `merge /topic1`. | ||
|
|
||
| foo/main> branch /topic2 | ||
|
|
||
| Done. I've created the topic2 branch based off of main. |
There was a problem hiding this comment.
unrelated issue, but maybe we want to use the slash syntax here too?
There was a problem hiding this comment.
I don't think so; the slash isn't part of the branch name. Maybe that's also an argument against using it in the "I merged /bob into /alice" output message 🤔
aryairani
reviewed
May 3, 2024
| & UF.hashTermsId | ||
| & Map.toList | ||
| & mapMaybe \(var, (_, ref, wk, _, _)) -> do | ||
| guard (WK.watchKindShouldBeStoredInDatabase wk) |
There was a problem hiding this comment.
It's keeping only these:
foo = ...
test> bar = ...
but not
> hey
nor
wat> x = ...
This reverts commit 9afdce5.
aryairani
reviewed
May 9, 2024
aryairani
reviewed
May 9, 2024
Co-authored-by: Arya Irani <538571+aryairani@users.noreply.github.com>
Co-authored-by: Arya Irani <538571+aryairani@users.noreply.github.com>
aryairani
approved these changes
May 16, 2024
|
Yay!!!!! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR contains the MVP / minimal thing / version 0 of the new merge algorithm.
See merge.output.md for an overview of its behavior.
In summary, we diff namespaces based on "syntactic hashes" in which a pretty-print environment renders references before hashing. This is the mechanism by which we distinguish "user changes" from auto-propagated changes.
There are a number of different preconditions that each namespace (and their LCA) must satisfy before we can attempt a merge, such as having no conflicted names, and having exactly one properly-placed name for each constructor of a particular naming of a data declaration. See the above transcript for more details.
A couple outstanding things:
mergestill exists (hidden) asmerge.old. Thepullcommand still performs amerge.oldafter downloading entities, not amerge.merge.previewnormerge.squash. Those still exist asmerge.old.previewandmerge.old.squash.mergeto instruct the user on how to resolve #4928And a note about the code quality:
honk,bonk, and perhapsoink. However, none of it was feeling like it should block the review of this PR. I plan to continue to refine things in the upcoming days.