Skip to content
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

merge precondition message: Conflict involving builtin #4980

Closed
Tracked by #4928
aryairani opened this issue May 20, 2024 · 0 comments · Fixed by #5032
Closed
Tracked by #4928

merge precondition message: Conflict involving builtin #4980

aryairani opened this issue May 20, 2024 · 0 comments · Fixed by #5032

Comments

@aryairani
Copy link
Contributor

aryairani commented May 20, 2024

Conflict involving builtin

We don't have a way of rendering a builtin in a scratch file, where users resolve merge conflicts. Thus, if there is a
conflict involving a builtin, we can't perform a merge.

One way to fix this in the future would be to introduce a syntax for defining aliases in the scratch file.

Alice's branch:

project/alice> alias.type builtin.Nat MyNat

  Done.

Bob's branch:

unique type MyNat = MyNat Nat
project/alice> merge /bob

  There's a merge conflict on MyNat, but it's a builtin on one
  or both branches. We can't yet handle merge conflicts on
  builtins.


Sorry, I wasn't able to perform the merge:

There's a merge conflict on MyNat, but it's a builtin on one or both branches. I can't yet handle merge conflicts involving builtins.

Please eliminate this conflict by updating one branch or the other, making MyNat the same on both branches, or making neither of them a builtin, and then try the merge again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant