mirror of
https://github.com/unisonweb/unison.git
synced 2024-10-05 14:17:33 +03:00
Merge pull request #5172 from unisonweb/cp/more-project-transcripts
This commit is contained in:
commit
a74d4e8cb9
@ -3,7 +3,7 @@
|
||||
https://github.com/unisonweb/unison/issues/2786
|
||||
|
||||
```ucm:hide
|
||||
.ns> builtins.merge
|
||||
scratch/main> builtins.merge lib.builtins
|
||||
```
|
||||
|
||||
First we add an ability to the codebase.
|
||||
@ -15,7 +15,7 @@ unique ability Channels where
|
||||
```
|
||||
|
||||
```ucm
|
||||
.ns> add
|
||||
scratch/main> add
|
||||
```
|
||||
|
||||
Now we update the ability, changing the name of the constructor, _but_, we simultaneously
|
||||
@ -36,8 +36,8 @@ thing _ = send 1
|
||||
These should fail with a term/ctor conflict since we exclude the ability from the update.
|
||||
|
||||
```ucm:error
|
||||
.ns> update.old patch Channels.send
|
||||
.ns> update.old patch thing
|
||||
scratch/main> update.old patch Channels.send
|
||||
scratch/main> update.old patch thing
|
||||
```
|
||||
|
||||
If however, `Channels.send` and `thing` _depend_ on `Channels`, updating them should succeed since it pulls in the ability as a dependency.
|
||||
@ -56,20 +56,20 @@ thing _ = send 1
|
||||
These updates should succeed since `Channels` is a dependency.
|
||||
|
||||
```ucm
|
||||
.ns> update.old.preview patch Channels.send
|
||||
.ns> update.old.preview patch thing
|
||||
scratch/main> update.old.preview patch Channels.send
|
||||
scratch/main> update.old.preview patch thing
|
||||
```
|
||||
|
||||
We should also be able to successfully update the whole thing.
|
||||
|
||||
```ucm
|
||||
.ns> update.old
|
||||
scratch/main> update.old
|
||||
```
|
||||
|
||||
# Constructor-term conflict
|
||||
|
||||
```ucm:hide
|
||||
.ns2> builtins.merge
|
||||
scratch/main2> builtins.merge lib.builtins
|
||||
```
|
||||
|
||||
|
||||
@ -78,7 +78,7 @@ X.x = 1
|
||||
```
|
||||
|
||||
```ucm
|
||||
.ns2> add
|
||||
scratch/main2> add
|
||||
```
|
||||
|
||||
```unison
|
||||
@ -89,5 +89,5 @@ structural ability X where
|
||||
This should fail with a ctor/term conflict.
|
||||
|
||||
```ucm:error
|
||||
.ns2> add
|
||||
scratch/main2> add
|
||||
```
|
||||
|
@ -24,7 +24,7 @@ unique ability Channels where
|
||||
|
||||
```
|
||||
```ucm
|
||||
.ns> add
|
||||
scratch/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
@ -68,7 +68,7 @@ thing _ = send 1
|
||||
These should fail with a term/ctor conflict since we exclude the ability from the update.
|
||||
|
||||
```ucm
|
||||
.ns> update.old patch Channels.send
|
||||
scratch/main> update.old patch Channels.send
|
||||
|
||||
x These definitions failed:
|
||||
|
||||
@ -77,7 +77,7 @@ These should fail with a term/ctor conflict since we exclude the ability from th
|
||||
|
||||
Tip: Use `help filestatus` to learn more.
|
||||
|
||||
.ns> update.old patch thing
|
||||
scratch/main> update.old patch thing
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
@ -122,7 +122,7 @@ thing _ = send 1
|
||||
These updates should succeed since `Channels` is a dependency.
|
||||
|
||||
```ucm
|
||||
.ns> update.old.preview patch Channels.send
|
||||
scratch/main> update.old.preview patch Channels.send
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
@ -135,7 +135,7 @@ These updates should succeed since `Channels` is a dependency.
|
||||
|
||||
Channels.send : a ->{Channels} ()
|
||||
|
||||
.ns> update.old.preview patch thing
|
||||
scratch/main> update.old.preview patch thing
|
||||
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
@ -153,7 +153,7 @@ These updates should succeed since `Channels` is a dependency.
|
||||
We should also be able to successfully update the whole thing.
|
||||
|
||||
```ucm
|
||||
.ns> update.old
|
||||
scratch/main> update.old
|
||||
|
||||
⊡ Ignored previously added definitions: Channels
|
||||
|
||||
@ -183,7 +183,7 @@ X.x = 1
|
||||
|
||||
```
|
||||
```ucm
|
||||
.ns2> add
|
||||
scratch/main2> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
@ -215,7 +215,7 @@ structural ability X where
|
||||
This should fail with a ctor/term conflict.
|
||||
|
||||
```ucm
|
||||
.ns2> add
|
||||
scratch/main2> add
|
||||
|
||||
x These definitions failed:
|
||||
|
||||
|
@ -19,8 +19,8 @@ f id = (id 1, id "hi")
|
||||
Another example, involving abilities. Here the ability-polymorphic function is instantiated with two different ability lists, `{}` and `{IO}`:
|
||||
|
||||
```unison
|
||||
f : (forall a g . '{g} a -> '{g} a) -> () -> ()
|
||||
f id _ =
|
||||
f : (forall a g . '{g} a -> '{g} a) -> () -> ()
|
||||
f id _ =
|
||||
_ = (id ('1 : '{} Nat), id ('("hi") : '{IO} Text))
|
||||
()
|
||||
```
|
||||
@ -34,17 +34,17 @@ Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b)
|
||||
Functor.map = cases Functor f -> f
|
||||
|
||||
Functor.blah : Functor f -> ()
|
||||
Functor.blah = cases Functor f ->
|
||||
Functor.blah = cases Functor f ->
|
||||
g : forall a b . (a -> b) -> f a -> f b
|
||||
g = f
|
||||
()
|
||||
```
|
||||
|
||||
This example is similar, but involves abilities:
|
||||
This example is similar, but involves abilities:
|
||||
|
||||
```unison
|
||||
unique ability Remote t where doRemoteStuff : t ()
|
||||
unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a)
|
||||
unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a)
|
||||
|
||||
Loc.blah : Loc -> ()
|
||||
Loc.blah = cases Loc f ->
|
||||
@ -52,20 +52,20 @@ Loc.blah = cases Loc f ->
|
||||
f0 = f
|
||||
()
|
||||
|
||||
-- In this case, no annotation is needed since the lambda
|
||||
-- In this case, no annotation is needed since the lambda
|
||||
-- is checked against a polymorphic type
|
||||
Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
-> Loc -> Loc
|
||||
Loc.transform nt = cases Loc f -> Loc (a -> f (nt a))
|
||||
|
||||
-- In this case, the annotation is needed since f' is inferred
|
||||
-- on its own it won't infer the higher-rank type
|
||||
Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
-> Loc -> Loc
|
||||
Loc.transform2 nt = cases Loc f ->
|
||||
Loc.transform2 nt = cases Loc f ->
|
||||
f' : forall t a . '{Remote t} a ->{Remote t} t a
|
||||
f' a = f (nt a)
|
||||
Loc f'
|
||||
Loc f'
|
||||
```
|
||||
|
||||
## Types with polymorphic fields
|
||||
@ -77,6 +77,6 @@ structural type HigherRanked = HigherRanked (forall a. a -> a)
|
||||
We should be able to add and view records with higher-rank fields.
|
||||
|
||||
```ucm
|
||||
.higher_ranked> add
|
||||
.higher_ranked> view HigherRanked
|
||||
scratch/main> add
|
||||
scratch/main> view HigherRanked
|
||||
```
|
||||
|
@ -33,8 +33,8 @@ f id = (id 1, id "hi")
|
||||
Another example, involving abilities. Here the ability-polymorphic function is instantiated with two different ability lists, `{}` and `{IO}`:
|
||||
|
||||
```unison
|
||||
f : (forall a g . '{g} a -> '{g} a) -> () -> ()
|
||||
f id _ =
|
||||
f : (forall a g . '{g} a -> '{g} a) -> () -> ()
|
||||
f id _ =
|
||||
_ = (id ('1 : '{} Nat), id ('("hi") : '{IO} Text))
|
||||
()
|
||||
```
|
||||
@ -61,7 +61,7 @@ Functor.map : Functor f -> (forall a b . (a -> b) -> f a -> f b)
|
||||
Functor.map = cases Functor f -> f
|
||||
|
||||
Functor.blah : Functor f -> ()
|
||||
Functor.blah = cases Functor f ->
|
||||
Functor.blah = cases Functor f ->
|
||||
g : forall a b . (a -> b) -> f a -> f b
|
||||
g = f
|
||||
()
|
||||
@ -83,11 +83,11 @@ Functor.blah = cases Functor f ->
|
||||
-> (∀ a b. (a -> b) -> f a -> f b)
|
||||
|
||||
```
|
||||
This example is similar, but involves abilities:
|
||||
This example is similar, but involves abilities:
|
||||
|
||||
```unison
|
||||
unique ability Remote t where doRemoteStuff : t ()
|
||||
unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a)
|
||||
unique type Loc = Loc (forall t a . '{Remote t} a ->{Remote t} t a)
|
||||
|
||||
Loc.blah : Loc -> ()
|
||||
Loc.blah = cases Loc f ->
|
||||
@ -95,20 +95,20 @@ Loc.blah = cases Loc f ->
|
||||
f0 = f
|
||||
()
|
||||
|
||||
-- In this case, no annotation is needed since the lambda
|
||||
-- In this case, no annotation is needed since the lambda
|
||||
-- is checked against a polymorphic type
|
||||
Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
Loc.transform : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
-> Loc -> Loc
|
||||
Loc.transform nt = cases Loc f -> Loc (a -> f (nt a))
|
||||
|
||||
-- In this case, the annotation is needed since f' is inferred
|
||||
-- on its own it won't infer the higher-rank type
|
||||
Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
Loc.transform2 : (forall t a . '{Remote t} a -> '{Remote t} a)
|
||||
-> Loc -> Loc
|
||||
Loc.transform2 nt = cases Loc f ->
|
||||
Loc.transform2 nt = cases Loc f ->
|
||||
f' : forall t a . '{Remote t} a ->{Remote t} t a
|
||||
f' a = f (nt a)
|
||||
Loc f'
|
||||
Loc f'
|
||||
```
|
||||
|
||||
```ucm
|
||||
@ -141,15 +141,13 @@ structural type HigherRanked = HigherRanked (forall a. a -> a)
|
||||
We should be able to add and view records with higher-rank fields.
|
||||
|
||||
```ucm
|
||||
☝️ The namespace .higher_ranked is empty.
|
||||
|
||||
.higher_ranked> add
|
||||
scratch/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
structural type HigherRanked
|
||||
|
||||
.higher_ranked> view HigherRanked
|
||||
scratch/main> view HigherRanked
|
||||
|
||||
structural type HigherRanked = HigherRanked (∀ a. a -> a)
|
||||
|
||||
|
@ -4,8 +4,8 @@ The `merge` command merges together two branches in the same project: the curren
|
||||
branch. For example, to merge `topic` into `main`, switch to `main` and run `merge topic`:
|
||||
|
||||
```ucm:error
|
||||
.> help merge
|
||||
.> help merge.commit
|
||||
scratch/main> help merge
|
||||
scratch/main> help merge.commit
|
||||
```
|
||||
|
||||
Let's see a simple unconflicted merge in action: Alice (us) and Bob (them) add different terms. The merged result
|
||||
|
@ -4,12 +4,12 @@ The `merge` command merges together two branches in the same project: the curren
|
||||
branch. For example, to merge `topic` into `main`, switch to `main` and run `merge topic`:
|
||||
|
||||
```ucm
|
||||
.> help merge
|
||||
scratch/main> help merge
|
||||
|
||||
merge
|
||||
`merge /branch` merges `branch` into the current branch
|
||||
|
||||
.> help merge.commit
|
||||
scratch/main> help merge.commit
|
||||
|
||||
merge.commit (or commit.merge)
|
||||
`merge.commit` merges a temporary branch created by the `merge`
|
||||
|
@ -15,7 +15,7 @@ two.ambiguousTerm = "term two"
|
||||
```
|
||||
|
||||
```ucm
|
||||
.example.resolution_failures> add
|
||||
scratch/main> add
|
||||
```
|
||||
|
||||
## Tests
|
||||
|
@ -31,9 +31,7 @@ two.ambiguousTerm = "term two"
|
||||
|
||||
```
|
||||
```ucm
|
||||
☝️ The namespace .example.resolution_failures is empty.
|
||||
|
||||
.example.resolution_failures> add
|
||||
scratch/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
|
@ -3,8 +3,7 @@
|
||||
Updating conflicted definitions works fine.
|
||||
|
||||
```ucm:hide
|
||||
.> builtins.merge
|
||||
.merged> builtins.merge
|
||||
scratch/main> builtins.merge lib.builtins
|
||||
```
|
||||
|
||||
```unison
|
||||
@ -13,9 +12,9 @@ temp = 2
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> add
|
||||
.> debug.alias.term.force temp x
|
||||
.> delete.term temp
|
||||
scratch/main> add
|
||||
scratch/main> debug.alias.term.force temp x
|
||||
scratch/main> delete.term temp
|
||||
```
|
||||
|
||||
```unison
|
||||
@ -23,6 +22,6 @@ x = 3
|
||||
```
|
||||
|
||||
```ucm
|
||||
.> update
|
||||
.> view x
|
||||
scratch/main> update
|
||||
scratch/main> view x
|
||||
```
|
||||
|
@ -22,18 +22,18 @@ temp = 2
|
||||
|
||||
```
|
||||
```ucm
|
||||
.> add
|
||||
scratch/main> add
|
||||
|
||||
⍟ I've added these definitions:
|
||||
|
||||
temp : Nat
|
||||
x : Nat
|
||||
|
||||
.> debug.alias.term.force temp x
|
||||
scratch/main> debug.alias.term.force temp x
|
||||
|
||||
Done.
|
||||
|
||||
.> delete.term temp
|
||||
scratch/main> delete.term temp
|
||||
|
||||
Done.
|
||||
|
||||
@ -57,14 +57,14 @@ x = 3
|
||||
|
||||
```
|
||||
```ucm
|
||||
.> update
|
||||
scratch/main> update
|
||||
|
||||
Okay, I'm searching the branch for code that needs to be
|
||||
updated...
|
||||
|
||||
Done.
|
||||
|
||||
.> view x
|
||||
scratch/main> view x
|
||||
|
||||
x : Nat
|
||||
x = 3
|
||||
|
Loading…
Reference in New Issue
Block a user