-
Notifications
You must be signed in to change notification settings - Fork 272
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add reproductions for several issues
- Loading branch information
Arya Irani
committed
Dec 16, 2024
1 parent
f9cc70e
commit e9e335c
Showing
9 changed files
with
663 additions
and
0 deletions.
There are no files selected for viewing
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,70 @@ | ||
``` ucm :hide | ||
scratch/main> builtins.merge | ||
``` | ||
|
||
If you | ||
|
||
``` unison | ||
foo.bar : Nat | ||
foo.bar = 17 | ||
``` | ||
|
||
``` ucm :added-by-ucm | ||
Loading changes detected in scratch.u. | ||
I found and typechecked these definitions in scratch.u. If you | ||
do an `add` or `update`, here's how your codebase would | ||
change: | ||
⍟ These new definitions are ok to `add`: | ||
foo.bar : Nat | ||
``` | ||
|
||
``` ucm :hide | ||
scratch/main> add | ||
``` | ||
|
||
and then put this into `scratch.u`, you'll see a scary message that says `update` will fail: | ||
|
||
``` unison | ||
unique type foo = bar | ||
``` | ||
|
||
``` ucm :added-by-ucm | ||
Loading changes detected in scratch.u. | ||
I found and typechecked these definitions in scratch.u. If you | ||
do an `add` or `update`, here's how your codebase would | ||
change: | ||
x These definitions would fail on `add` or `update`: | ||
Reason | ||
blocked type foo | ||
ctor/term collision foo.bar | ||
Tip: Use `help filestatus` to learn more. | ||
``` | ||
|
||
... but `update` doesn't fail. | ||
|
||
``` ucm | ||
scratch/main> update | ||
Okay, I'm searching the branch for code that needs to be | ||
updated... | ||
Done. | ||
``` | ||
|
||
Now we have one name `foo.bar` that refers to two things. | ||
|
||
``` ucm | ||
scratch/main> view foo.bar | ||
type foo = bar#ls59rkdkv5#0 | ||
foo.bar#cq22mm4sca : Nat | ||
foo.bar#cq22mm4sca = 17 | ||
``` |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
Suggestion: | ||
|
||
Since it doesn't work anyway, we should disable adding or updating definitions under lib. | ||
|
||
``` ucm :hide | ||
scratch/main> alias.type ##Nat lib.builtin.Nat | ||
``` | ||
|
||
``` unison | ||
lib.foo.bar : Nat | ||
lib.foo.bar = 17 | ||
``` | ||
|
||
``` ucm :added-by-ucm | ||
Loading changes detected in scratch.u. | ||
I found and typechecked these definitions in scratch.u. If you | ||
do an `add` or `update`, here's how your codebase would | ||
change: | ||
⍟ These new definitions are ok to `add`: | ||
lib.foo.bar : Nat | ||
``` | ||
|
||
``` ucm | ||
scratch/main> add | ||
⍟ I've added these definitions: | ||
lib.foo.bar : Nat | ||
``` | ||
|
||
Arguments against: | ||
We probably use this feature currently to set up transcripts, etc. A workaround could cbe setting up the mock libs in a separate branch and then using the "use branch as lib" mechanism. (Currently `fork` iirc, and eventually something else when we have first-class-ier dependencies.) |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,98 @@ | ||
In this example, Alice updates `foo`, while Bob adds a new dependent `bar` of the original `foo`. When Bob's branch is merged into Alice's, her update to `foo` is propagated to his `bar`. | ||
|
||
``` ucm :hide | ||
project/main> builtins.mergeio | ||
``` | ||
|
||
Initial branch: | ||
|
||
``` unison :hide | ||
foo : Text | ||
foo = "old foo" | ||
``` | ||
|
||
``` ucm :hide | ||
project/main> add | ||
project/main> branch alice | ||
``` | ||
|
||
Alice's updates: | ||
|
||
``` unison :hide | ||
foo : Text | ||
foo = "new foo" | ||
``` | ||
|
||
``` ucm :hide | ||
project/alice> update | ||
project/main> branch bob | ||
``` | ||
|
||
Bob's adds: | ||
|
||
``` unison :hide | ||
bar : Text | ||
bar = foo ++ " - " ++ foo | ||
``` | ||
|
||
``` ucm | ||
project/bob> display bar | ||
"old foo - old foo" | ||
``` | ||
|
||
``` ucm :hide | ||
project/bob> add | ||
``` | ||
|
||
If we merge /bob into /alice, we'd expect `bar` to be updated with Alice's change: | ||
|
||
``` ucm | ||
project/alice> merge /bob | ||
Loading branches... | ||
Computing diff between branches... | ||
Loading dependents of changes... | ||
Loading and merging library dependencies... | ||
Rendering Unison file... | ||
Typechecking Unison file... | ||
I merged project/bob into project/alice. | ||
project/alice> view foo bar | ||
bar : Text | ||
bar = | ||
use Text ++ | ||
foo ++ " - " ++ foo | ||
foo : Text | ||
foo = "new foo" | ||
project/alice> display foo bar | ||
"new foo" | ||
"old foo - old foo" | ||
``` | ||
|
||
But then, bafflingly, if you restart ucm with this same codebase, `display foo bar` will show the new definition, meaning that somehow the in-memory results are out of sync with what's actually in the databse? | ||
|
||
``` bash | ||
$ ucm transcript --save-codebase transcripts/idempotent/repro4921.md | ||
$ ucm --codebase /private/var/folders/7j/rwwnwnyn0djb5tw9bnxhd5bc0000gn/T/transcript-e39aecc3fc26a4dd #for example | ||
# <snip> | ||
# project/alice> display foo bar | ||
# | ||
# "new foo" | ||
# | ||
# | ||
# "new foo - new foo" | ||
``` |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
This gives a confusing error for a subtle reason. | ||
|
||
``` unison :error | ||
type CompressionMethod = | ||
type ConnectionState = { compressionMethod: CompressionMethod} | ||
``` | ||
|
||
``` ucm :added-by-ucm | ||
Loading changes detected in scratch.u. | ||
This case would be ignored because it's already covered by the preceding case(s): | ||
3 | type ConnectionState = { compressionMethod: CompressionMethod} | ||
``` | ||
|
||
It's confusing because there's no case shown (the pattern-matching code at issue is synthetic and hidden), and no preceding case(s) either. | ||
|
||
Here it is without any record syntax: | ||
|
||
``` unison :error | ||
type X = | ||
type A = A1 X | ||
ax = cases | ||
A1 x -> x | ||
``` | ||
|
||
``` ucm :added-by-ucm | ||
Loading changes detected in scratch.u. | ||
This case would be ignored because it's already covered by the preceding case(s): | ||
6 | A1 x -> x | ||
``` | ||
|
||
It's trying to say that the pattern `A1 x` can never be matched because `A1` can never be used, because `X` can't be instantiated, because there are no constructors for it. |
Oops, something went wrong.