unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-08-15 13:30:27 +03:00
Code Issues Projects Releases Wiki Activity

Delete some out of date bits of transcripts

Browse Source
This commit is contained in:
Chris Penner 2024-06-27 15:01:58 -07:00
parent dadc4e476b
commit 0b8548f36c
5 changed files with 202 additions and 439 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
unison-src/transcripts/cycle-update-5.md
View File

@ -1,34 +0,0 @@
Not yet working: properly updating nameless implicit terms.
```ucm:hide
scratch/main> builtins.merge
```
```unison
inner.ping : 'Nat
inner.ping _ = !pong + 1
pong : 'Nat
pong _ = !inner.ping + 2
```
```ucm
scratch/main> add
```
Here we queue up an update by saving in a namespace where `inner.ping` and `pong` both have names, but then apply the
update in a namespace where only `ping` has a name.
```unison
inner.ping : 'Nat
inner.ping _ = !pong + 3
```
```ucm
.inner> update.old
scratch/main> view inner.ping
```
The bug here is that `inner.ping` still refers to `pong` by name. But if we properly identified the nameless (in the
context that the update was applied) `pong` as an implicit term to include in the new `ping`'s cycle, then `ping` would
be left referring to a nameless thing (namely, `pong`, but updated to refer to the new `ping`).

82
unison-src/transcripts/cycle-update-5.output.md
View File

@ -1,82 +0,0 @@
Not yet working: properly updating nameless implicit terms.
```unison
inner.ping : 'Nat
inner.ping _ = !pong + 1
pong : 'Nat
pong _ = !inner.ping + 2
```
```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`:
inner.ping : 'Nat
pong : 'Nat
```
```ucm
scratch/main> add
⍟ I've added these definitions:
inner.ping : 'Nat
pong : 'Nat
```
Here we queue up an update by saving in a namespace where `inner.ping` and `pong` both have names, but then apply the
update in a namespace where only `ping` has a name.
```unison
inner.ping : 'Nat
inner.ping _ = !pong + 3
```
```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 names already exist. You can `update` them to your
new definition:
inner.ping : 'Nat
```
```ucm
☝️ The namespace .inner is empty.
.inner> update.old
⍟ I've added these definitions:
inner.ping : '##Nat
scratch/main> view inner.ping
<<<<<<< Conflict 1 of 1
%%%%%%% Changes from base to side #1
inner.ping : 'Nat
inner.ping _ =
use Nat +
- !pong + 1
+ pong() + 1
+++++++ Contents of side #2
inner.inner.ping : '##Nat
inner.inner.ping _ = ##Nat.+ !#4t465jk908 3
>>>>>>> Conflict 1 of 1 ends
```
The bug here is that `inner.ping` still refers to `pong` by name. But if we properly identified the nameless (in the
context that the update was applied) `pong` as an implicit term to include in the new `ping`'s cycle, then `ping` would
be left referring to a nameless thing (namely, `pong`, but updated to refer to the new `ping).

234
unison-src/transcripts/fix2254.output.md
View File

@ -37,7 +37,7 @@ We'll make our edits in a new branch.
scratch/a> add
⍟ I've added these definitions:
type A a b c d
structural type NeedsA a b
f : A Nat Nat Nat Nat -> Nat
@ -70,84 +70,95 @@ Let's do the update now, and verify that the definitions all look good and there
scratch/a2> update.old
⍟ I've updated these names to your new definition:
type A a b c d
scratch/a2> view A NeedsA f f2 f3 g
<<<<<<< Conflict 1 of 5
%%%%%%% Changes from base to side #1
type A a b c d
- = B b
+ = A a
| D d
| E a d
+ | B b
| C c
- | A a
structural type NeedsA a b
- = Zoink Text
- | NeedsA (A a b Nat Nat)
+ = NeedsA (A a b Nat Nat)
+ | Zoink Text
f : A Nat Nat Nat Nat -> Nat
f = cases
A n -> n
_ -> 42
f2 : A Nat Nat Nat Nat -> Nat
f2 a =
use Nat +
n = f a
n + 1
f3 : NeedsA Nat Nat -> Nat
f3 = cases
NeedsA a -> f a Nat.+ 20
_ -> 0
g : A Nat Nat Nat Nat -> Nat
g = cases
D n -> n
_ -> 43
+++++++ Contents of side #2
type A a b c d = B b | D d | E a d | C c | A a
>>>>>>> Conflict 1 of 5 ends
type A a b c d
= A a
| D d
| E a d
| B b
| C c
structural type NeedsA a b
= NeedsA (A a b Nat Nat)
| Zoink Text
f : #re3rf9cedk Nat Nat Nat Nat -> Nat
f = cases
#re3rf9cedk#1 n -> n
_ -> 42
f2 : #re3rf9cedk Nat Nat Nat Nat -> Nat
f2 a =
use Nat +
n = f a
n + 1
f3 : #oftm6ao9vp Nat Nat -> Nat
f3 = cases
#oftm6ao9vp#0 a -> f a Nat.+ 20
_ -> 0
g : #re3rf9cedk Nat Nat Nat Nat -> Nat
g = cases
#re3rf9cedk#0 n -> n
_ -> 43
<<<<<<< Conflict 2 of 5
+++++++ Contents of side #1
scratch/a2> todo
%%%%%%% Changes from base to side #2
-.a2> todo
+ ⚠️
>>>>>>> Conflict 2 of 5 ends
The following names were not found in the codebase. Check your spelling.
NeedsA
f
f2
f3
g
These types do not have any names in the current namespace:
1. #oftm6ao9vp
2. #re3rf9cedk
```
## Record updates
Here's a test of updating a record:
```unison
structural type Rec = { uno : Nat, dos : Nat }
combine r = uno r + dos r
```
```ucm
.a2> update.old.a2> view A NeedsA f f2 f3 g.a2> todo
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`:
structural type Rec
Rec.dos : Rec -> Nat
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.dos.set : Nat -> Rec -> Rec
Rec.uno : Rec -> Nat
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.uno.set : Nat -> Rec -> Rec
combine : Rec -> Nat
```
<<<<<<< Conflict 3 of 5
+++++++ Contents of side #1
```ucm
scratch/r1> add
%%%%%%% Changes from base to side #2
-```ucm
-.a3> add
>>>>>>> Conflict 3 of 5 ends
⍟ I've added these definitions:
structural type Rec
Rec.dos : Rec -> Nat
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.dos.set : Nat -> Rec -> Rec
Rec.uno : Rec -> Nat
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.uno.set : Nat -> Rec -> Rec
combine : Rec -> Nat
<<<<<<< Conflict 4 of 5
+++++++ Contents of side #1
scratch/r1> branch r2
Done. I've created the r2 branch based off of r1.
@ -159,57 +170,56 @@ scratch/r1> branch r2
```unison
structural type Rec = { uno : Nat, dos : Nat, tres : Text }
```
%%%%%%% Changes from base to side #2
-```
-```unison
-structural type Rec = { uno : Nat, dos : Nat, tres : Text }
-```
+🛑
>>>>>>> Conflict 4 of 5 ends
The transcript failed due to an error in the stanza above. The error is:
```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`:
Rec.tres : Rec -> Text
Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
Rec.tres.set : Text -> Rec -> Rec
⍟ These names already exist. You can `update` them to your
new definition:
structural type Rec
Rec.dos : Rec -> Nat
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.dos.set : Nat -> Rec -> Rec
Rec.uno : Rec -> Nat
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.uno.set : Nat -> Rec -> Rec
The following names were not found in the codebase. Check your spelling.
NeedsA
f
f2
f3
g
```
And checking that after updating this record, there's nothing `todo`:
<<<<<<< Conflict 5 of 5
%%%%%%% Changes from base to side #1
```ucm
-.> fork a3 a4
+scratch/r2> update.old
- Done.
-
-.a4> update.old
-
⍟ I've added these definitions:
Rec.tres : Rec -> Text
Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
Rec.tres.set : Text -> Rec -> Rec
⍟ I've updated these names to your new definition:
structural type Rec
Rec.dos : Rec -> Nat
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.dos.set : Nat -> Rec -> Rec
Rec.uno : Rec -> Nat
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.uno.set : Nat -> Rec -> Rec
-.a4> todo
+scratch/r2> todo
```
+++++++ Contents of side #2
>>>>>>> Conflict 5 of 5 ends
```ucm
scratch/r2> update.old
⍟ I've added these definitions:
Rec.tres : Rec -> Text
Rec.tres.modify : (Text ->{g} Text) -> Rec ->{g} Rec
Rec.tres.set : Text -> Rec -> Rec
⍟ I've updated these names to your new definition:
structural type Rec
Rec.dos : Rec -> Nat
Rec.dos.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.dos.set : Nat -> Rec -> Rec
Rec.uno : Rec -> Nat
Rec.uno.modify : (Nat ->{g} Nat) -> Rec ->{g} Rec
Rec.uno.set : Nat -> Rec -> Rec
scratch/r2> todo
```

44
unison-src/transcripts/propagate.md
View File

@ -78,47 +78,3 @@ type of `otherTerm` should remain the same.
scratch/main> view preserve.someTerm
scratch/main> view preserve.otherTerm
```
### Propagation only applies to the local branch
Cleaning up a bit...
```ucm
.subpath.lib> builtins.merge
```
Now, we make two terms, where one depends on the other.
```unison
one.someTerm : Optional foo -> Optional foo
one.someTerm x = x
one.otherTerm : Optional baz -> Optional baz
one.otherTerm y = someTerm y
```
We'll make two copies of this namespace.
```ucm
.subpath> add
.subpath> fork one two
```
Now let's edit one of the terms...
```unison
someTerm : Optional x -> Optional x
someTerm _ = None
```
... in one of the namespaces...
```ucm
.subpath.one> update.old
```
The other namespace should be left alone.
```ucm
.subpath> view two.someTerm
```

247
unison-src/transcripts/propagate.output.md
View File

@ -87,178 +87,91 @@ scratch/main> update.old
```ucm
scratch/main> view fooToInt
⚠️
The following names were not found in the codebase. Check your spelling.
fooToInt
fooToInt : Foo -> Int
fooToInt _ = +42
```
### Preserving user type variables
We make a term that has a dependency on another term and also a non-redundant
user-provided type signature.
```unison
preserve.someTerm : Optional foo -> Optional foo
preserve.someTerm x = x
preserve.otherTerm : Optional baz -> Optional baz
preserve.otherTerm y = someTerm y
```
```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`:
preserve.otherTerm : Optional baz -> Optional baz
preserve.someTerm : Optional foo -> Optional foo
```
Add that to the codebase:
<<<<<<< Conflict 1 of 2
+++++++ Contents of side #1
```ucm
scratch/main> add
%%%%%%% Changes from base to side #2
-```ucm
-.subpath> add
>>>>>>> Conflict 1 of 2 ends
🛑
The transcript failed due to an error in the stanza above. The error is:
⚠️
⍟ I've added these definitions:
The following names were not found in the codebase. Check your spelling.
fooToInt
preserve.otherTerm : Optional baz -> Optional baz
preserve.someTerm : Optional foo -> Optional foo
<<<<<<< Conflict 2 of 2
%%%%%%% Changes from base to side #1
```
Let's now edit the dependency:
```unison
preserve.someTerm : Optional x -> Optional x
preserve.someTerm _ = None
```
```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 names already exist. You can `update` them to your
new definition:
preserve.someTerm : Optional x -> Optional x
```
Update...
```ucm
-.subpath> update.old
+scratch/main> update.old
⍟ I've updated these names to your new definition:
preserve.someTerm : Optional x -> Optional x
```
Now the type of `someTerm` should be `Optional x -> Optional x` and the
type of `otherTerm` should remain the same.
```ucm
-.subpath> view preserve.someTerm
+scratch/main> view preserve.someTerm
preserve.someTerm : Optional x -> Optional x
preserve.someTerm _ = None
-.subpath> view preserve.otherTerm
+scratch/main> view preserve.otherTerm
preserve.otherTerm : Optional baz -> Optional baz
preserve.otherTerm y = someTerm y
```
### Propagation only applies to the local branch
Cleaning up a bit...
```ucm
-.> delete.namespace subpath
-
- Done.
-
☝️ The namespace .subpath.lib is empty.
.subpath.lib> builtins.merge
Done.
```
Now, we make two terms, where one depends on the other.
```unison
one.someTerm : Optional foo -> Optional foo
one.someTerm x = x
one.otherTerm : Optional baz -> Optional baz
one.otherTerm y = someTerm y
```
```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`:
one.otherTerm : Optional baz -> Optional baz
one.someTerm : Optional foo -> Optional foo
```
We'll make two copies of this namespace.
```ucm
.subpath> add
⍟ I've added these definitions:
one.otherTerm : Optional baz -> Optional baz
one.someTerm : Optional foo -> Optional foo
.subpath> fork one two
Done.
```
Now let's edit one of the terms...
```unison
someTerm : Optional x -> Optional x
someTerm _ = None
```
```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`:
someTerm : Optional x -> Optional x
```
... in one of the namespaces...
```ucm
.subpath.one> update.old
⍟ I've updated these names to your new definition:
someTerm : #nirp5os0q6 x -> #nirp5os0q6 x
```
The other namespace should be left alone.
```ucm
.subpath> view two.someTerm
two.someTerm : Optional foo -> Optional foo
two.someTerm x = x
```
+++++++ Contents of side #2
>>>>>>> Conflict 2 of 2 ends
```
Let's now edit the dependency:
```unison
preserve.someTerm : Optional x -> Optional x
preserve.someTerm _ = None
```
```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 names already exist. You can `update` them to your
new definition:
preserve.someTerm : Optional x -> Optional x
```
Update...
```ucm
scratch/main> update.old
⍟ I've updated these names to your new definition:
preserve.someTerm : Optional x -> Optional x
```
Now the type of `someTerm` should be `Optional x -> Optional x` and the
type of `otherTerm` should remain the same.
```ucm
scratch/main> view preserve.someTerm
preserve.someTerm : Optional x -> Optional x
preserve.someTerm _ = None
scratch/main> view preserve.otherTerm
preserve.otherTerm : Optional baz -> Optional baz
preserve.otherTerm y = someTerm y
```