never assume builtins are known to the db

fixes 107 failing transcripts
This commit is contained in:
Arya Irani 2021-12-06 11:26:37 -10:00
parent 6055ca6184
commit 52b2c81783
25 changed files with 226 additions and 219 deletions

View File

@ -249,7 +249,6 @@ data Error
= DecodeError DecodeError ByteString ErrString
| DatabaseIntegrityError Q.Integrity
| UnknownDependency H.Hash
| UnknownText Text
| ExpectedBranch CausalHash BranchHash
| ExpectedBranch' Db.CausalHashId
| LegacyUnknownCycleLen H.Hash
@ -270,12 +269,6 @@ liftQ a =
-- * Database lookups
lookupTextId :: EDB m => Text -> m Db.TextId
lookupTextId t =
Q.loadText t >>= \case
Just textId -> pure textId
Nothing -> throwError $ UnknownText t
loadTextById :: EDB m => Db.TextId -> m Text
loadTextById = liftQ . Q.loadTextById
@ -335,8 +328,11 @@ loadMaybeRootCausalHash =
-- ** read existing references
-- |Assumes that a derived reference would already exist in the database
-- (by virtue of dependencies being stored before dependents), but does
-- not assume a builtin reference would.
c2sReference :: EDB m => C.Reference -> m S.Reference
c2sReference = bitraverse lookupTextId primaryHashToExistingObjectId
c2sReference = bitraverse Q.saveText primaryHashToExistingObjectId
s2cReference :: EDB m => S.Reference -> m C.Reference
s2cReference = bitraverse loadTextById loadHashByObjectId

View File

@ -335,16 +335,18 @@ and the rendered output using `display`:
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
@ -637,16 +639,18 @@ Lastly, it's common to build longer documents including subdocuments via `{{ sub
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x

View File

@ -106,11 +106,11 @@ ex5 = crypto.hmac Sha2_256 mysecret f |> hex
25 | > ex4
"c9adb8fbda582aeab113379dbd8f6af3ea450df1782780d61d44ad1ef7bff76e"
"c0fb39ed837cfe691bda9944b0c01a1c8c09dfc1be8d8501848d8d8d7651dcaf"
26 | > ex5
"b198a72da9e6c11536c0a2118002760a9eac57db7f9a0ce9ebda8cd8a806bd06"
"e04090fa634d01ecc7db4422b3611735170930bc7ef3ebcdb8b4f3cf778f7475"
```
And here's the full API:

View File

@ -29,7 +29,7 @@ test> match (decodeCert.impl (toUtf8 self_signed_cert_pem) with
⍟ These new definitions are ok to `add`:
test.ko630itb5m (Unison bug, unknown term)
test.cf6t0id1ti (Unison bug, unknown term)
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.

View File

@ -88,16 +88,18 @@ We can display the guide before and after adding it to the codebase:
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
@ -289,16 +291,18 @@ We can display the guide before and after adding it to the codebase:
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
@ -496,16 +500,18 @@ rendered = Pretty.get (docFormatConsole doc.guide)
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
@ -690,16 +696,18 @@ rendered = Pretty.get (docFormatConsole doc.guide)
Unison definitions can be included in docs. For instance:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x
Some rendering targets also support folded source:
structural type Optional a = Some a | None
structural type Optional a = None | Some a
sqr : Nat -> Nat
sqr x =
use Nat *
x * x

View File

@ -67,9 +67,9 @@ Test that replace works with types
.scratch> view.patch patch
Edited Types: X#d97e0jhkmd -> X
Edited Types: X#hhc6goudjq -> X
Edited Terms: #jk19sm5bf8 -> x
Edited Terms: #rrsqv1ogaq -> x
Tip: To remove entries from a patch, use
delete.term-replacement or delete.type-replacement, as

View File

@ -76,7 +76,7 @@ I should be able to view an affected dependency by number
dependents.usage1 : Nat
dependents.usage1 =
use Nat +
#jk19sm5bf8 + #0ja1qfpej6
#rrsqv1ogaq + #0t5t522gs3
```
Deleting the root namespace should require confirmation if not forced.

View File

@ -49,7 +49,7 @@ structural type Foo = Foo Nat
Removed definitions:
1. Foo.Foo : Nat -> #d97e0jhkmd
1. Foo.Foo : Nat -> #hhc6goudjq
Tip: You can use `undo` or `reflog` to undo this change.
@ -90,10 +90,10 @@ foo = 2
New name conflicts:
1. foo#jk19sm5bf8 : Nat
1. foo#rrsqv1ogaq : Nat
2. ┌ foo#0ja1qfpej6 : Nat
3. └ foo#jk19sm5bf8 : Nat
2. ┌ foo#0t5t522gs3 : Nat
3. └ foo#rrsqv1ogaq : Nat
Tip: You can use `todo` to see if this generated any work to
do in this namespace and `test` to run the tests. Or you
@ -108,13 +108,13 @@ A delete should remove both versions of the term.
Removed definitions:
1. a.foo#jk19sm5bf8 : Nat
1. a.foo#rrsqv1ogaq : Nat
Name changes:
Original Changes
2. b.foo ┐ 3. a.foo#0ja1qfpej6 (removed)
4. a.foo#0ja1qfpej6
2. b.foo ┐ 3. a.foo#0t5t522gs3 (removed)
4. a.foo#0t5t522gs3
Tip: You can use `undo` or `reflog` to undo this change.
@ -157,18 +157,18 @@ structural type Foo = Foo Boolean
New name conflicts:
1. structural type Foo#d97e0jhkmd
1. structural type Foo#hhc6goudjq
2. ┌ structural type Foo#d97e0jhkmd
2. ┌ structural type Foo#gf6ne3ran5
3. └ structural type Foo#gq9inhvg9h
3. └ structural type Foo#hhc6goudjq
4. Foo.Foo#d97e0jhkmd#0 : Nat -> Foo#d97e0jhkmd
4. Foo.Foo#hhc6goudjq#0 : Nat -> Foo#hhc6goudjq
5. ┌ Foo.Foo#d97e0jhkmd#0 : Nat -> Foo#d97e0jhkmd
6. └ Foo.Foo#gq9inhvg9h#0 : Boolean -> Foo#gq9inhvg9h
5. ┌ Foo.Foo#gf6ne3ran5#0 : Boolean -> Foo#gf6ne3ran5
6. └ Foo.Foo#hhc6goudjq#0 : Nat -> Foo#hhc6goudjq
Tip: You can use `todo` to see if this generated any work to
do in this namespace and `test` to run the tests. Or you
@ -181,13 +181,13 @@ structural type Foo = Foo Boolean
Removed definitions:
1. structural type a.Foo#d97e0jhkmd
1. structural type a.Foo#hhc6goudjq
Name changes:
Original Changes
2. b.Foo ┐ 3. a.Foo#gq9inhvg9h (removed)
4. a.Foo#gq9inhvg9h
2. b.Foo ┐ 3. a.Foo#gf6ne3ran5 (removed)
4. a.Foo#gf6ne3ran5
Tip: You can use `undo` or `reflog` to undo this change.
@ -197,13 +197,13 @@ structural type Foo = Foo Boolean
Removed definitions:
1. a.Foo.Foo#d97e0jhkmd#0 : Nat -> #d97e0jhkmd
1. a.Foo.Foo#hhc6goudjq#0 : Nat -> #hhc6goudjq
Name changes:
Original Changes
2. b.Foo.Foo ┐ 3. a.Foo.Foo#gq9inhvg9h#0 (removed)
4. a.Foo.Foo#gq9inhvg9h#0 ┘
2. b.Foo.Foo ┐ 3. a.Foo.Foo#gf6ne3ran5#0 (removed)
4. a.Foo.Foo#gf6ne3ran5#0 ┘
Tip: You can use `undo` or `reflog` to undo this change.

View File

@ -17,14 +17,14 @@ inside.r = d
```ucm
.> debug.file
type inside.M#ld0okei52l
type outside.A#e6mpjfecmg
type outside.B#muulibntaq
inside.p#fiupm7pl7o
inside.q#l5pndeifuh
inside.r#im2kiu2hmn
outside.c#msp7bv40rv
outside.d#6cdi7g1oi2
type inside.M#goba2va40r
type outside.A#ihqhr4prbp
type outside.B#mm8h095nrg
inside.p#h63obi5rb4
inside.q#1qtbral9uo
inside.r#9guss29ljv
outside.c#fs7la111vn
outside.d#p7dvt0ka99
```
This will help me make progress in some situations when UCM is being deficient or broken.
@ -47,47 +47,49 @@ But wait, there's more. I can check the dependencies and dependents of a defini
.> dependents q
#l5pndeifuh doesn't have any named dependents.
#1qtbral9uo doesn't have any named dependents.
.> dependencies q
Dependencies of #l5pndeifuh:
Dependencies of #1qtbral9uo:
Reference Name
1. ##Nat.* builtin.Nat.*
2. ##Nat.+ builtin.Nat.+
3. #fiupm7pl7o inside.p
1. ##Nat builtin.Nat
2. ##Nat.* builtin.Nat.*
3. ##Nat.+ builtin.Nat.+
4. #h63obi5rb4 inside.p
.> dependencies B
Dependencies of #muulibntaq:
Dependencies of #mm8h095nrg:
Reference Name
1. ##Int builtin.Int
Dependencies of #muulibntaq#0:
Dependencies of #mm8h095nrg#0:
Reference Name
1. #muulibntaq outside.B
1. #mm8h095nrg outside.B
2. ##Int builtin.Int
.> dependencies d
Dependencies of #6cdi7g1oi2:
Dependencies of #p7dvt0ka99:
Reference Name
1. ##Nat builtin.Nat
2. ##Nat.+ builtin.Nat.+
3. ##Universal.< builtin.Universal.<
4. #msp7bv40rv outside.c
5. #fiupm7pl7o inside.p
1. ##Boolean builtin.Boolean
2. ##Nat builtin.Nat
3. ##Nat.+ builtin.Nat.+
4. ##Universal.< builtin.Universal.<
5. #fs7la111vn outside.c
6. #h63obi5rb4 inside.p
.> dependents d
Dependents of #6cdi7g1oi2:
Dependents of #p7dvt0ka99:
Reference Name
1. #im2kiu2hmn inside.r
1. #9guss29ljv inside.r
```
We don't have an index for dependents of constructors, but iirc if you ask for that, it will show you dependents of the structural type that provided the constructor.

View File

@ -43,10 +43,10 @@ fslkdjflskdjflksjdf = 663
New name conflicts:
1. fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
1. fslkdjflskdjflksjdf#4vn50bh8pk : Nat
2. ┌ fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
3. └ fslkdjflskdjflksjdf#s5tu4n7rlb : Nat
2. ┌ fslkdjflskdjflksjdf#4vn50bh8pk : Nat
3. └ fslkdjflskdjflksjdf#9mupj24g1n : Nat
Tip: You can use `todo` to see if this generated any work to
do in this namespace and `test` to run the tests. Or you
@ -57,33 +57,33 @@ fslkdjflskdjflksjdf = 663
Resolved name conflicts:
1. ┌ fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
2. └ fslkdjflskdjflksjdf#s5tu4n7rlb : Nat
1. ┌ fslkdjflskdjflksjdf#4vn50bh8pk : Nat
2. └ fslkdjflskdjflksjdf#9mupj24g1n : Nat
3. fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
3. fslkdjflskdjflksjdf#4vn50bh8pk : Nat
Name changes:
Original Changes
4. x ┐ 5. abc (added)
6. fslkdjflskdjflksjdf#4kipsv2tm6 ┘ 7. fslkdjflskdjflksjdf (added)
8. fslkdjflskdjflksjdf#4kipsv2tm6 (removed)
6. fslkdjflskdjflksjdf#4vn50bh8pk ┘ 7. fslkdjflskdjflksjdf (added)
8. fslkdjflskdjflksjdf#4vn50bh8pk (removed)
.b2> diff.namespace .b1
Resolved name conflicts:
1. ┌ fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
2. └ fslkdjflskdjflksjdf#s5tu4n7rlb : Nat
1. ┌ fslkdjflskdjflksjdf#4vn50bh8pk : Nat
2. └ fslkdjflskdjflksjdf#9mupj24g1n : Nat
3. fslkdjflskdjflksjdf#4kipsv2tm6 : Nat
3. fslkdjflskdjflksjdf#4vn50bh8pk : Nat
Name changes:
Original Changes
4. x ┐ 5. abc (added)
6. fslkdjflskdjflksjdf#4kipsv2tm6 ┘ 7. fslkdjflskdjflksjdf (added)
8. fslkdjflskdjflksjdf#4kipsv2tm6 (removed)
6. fslkdjflskdjflksjdf#4vn50bh8pk ┘ 7. fslkdjflskdjflksjdf (added)
8. fslkdjflskdjflksjdf#4vn50bh8pk (removed)
```
Things we want to test:
@ -184,10 +184,10 @@ fromJust = "asldkfjasldkfj"
New name conflicts:
1. fromJust#jk19sm5bf8 : Nat
1. fromJust#rrsqv1ogaq : Nat
2. ┌ fromJust#hs2i9lcgkd : Text
3. └ fromJust#jk19sm5bf8 : Nat
2. ┌ fromJust#8vv2a5jnig : Text
3. └ fromJust#rrsqv1ogaq : Nat
Tip: You can use `todo` to see if this generated any work to
do in this namespace and `test` to run the tests. Or you
@ -232,10 +232,10 @@ unique type Y a b = Y a b
Resolved name conflicts:
1. ┌ fromJust#hs2i9lcgkd : Text
2. └ fromJust#jk19sm5bf8 : Nat
1. ┌ fromJust#8vv2a5jnig : Text
2. └ fromJust#rrsqv1ogaq : Nat
3. fromJust#1o1iq26cq7 : Nat
3. fromJust#mkj3tehhkv : Nat
- 4. ns1.b : Nat
+ 5. ns2.b : Text
@ -251,8 +251,6 @@ unique type Y a b = Y a b
- 10. ns1.b : Nat
+ 11. ns2.b : Text
There were 1 auto-propagated updates.
Added definitions:
12. unique type Y a b
@ -279,10 +277,10 @@ unique type Y a b = Y a b
Resolved name conflicts:
1. ┌ fromJust#hs2i9lcgkd : Text
2. └ fromJust#jk19sm5bf8 : Nat
1. ┌ fromJust#8vv2a5jnig : Text
2. └ fromJust#rrsqv1ogaq : Nat
3. fromJust#1o1iq26cq7 : Nat
3. fromJust#mkj3tehhkv : Nat
- 4. ns1.b : Nat
+ 5. ns2.b : Text
@ -298,8 +296,6 @@ unique type Y a b = Y a b
- 10. ns1.b : Nat
+ 11. ns2.b : Text
There were 1 auto-propagated updates.
Added definitions:
12. unique type Y a b
@ -336,10 +332,10 @@ unique type Y a b = Y a b
Resolved name conflicts:
1. ┌ fromJust#hs2i9lcgkd : Text
2. └ fromJust#jk19sm5bf8 : Nat
1. ┌ fromJust#8vv2a5jnig : Text
2. └ fromJust#rrsqv1ogaq : Nat
3. fromJust#1o1iq26cq7 : Nat
3. fromJust#mkj3tehhkv : Nat
- 4. ns1.b : Nat
+ 5. ns2.b : Text
@ -358,8 +354,6 @@ unique type Y a b = Y a b
- 12. ns1.b : Nat
+ 13. ns2.b : Text
There were 1 auto-propagated updates.
Added definitions:
14. unique type Y a b
@ -386,10 +380,10 @@ unique type Y a b = Y a b
Resolved name conflicts:
1. ┌ fromJust#hs2i9lcgkd : Text
2. └ fromJust#jk19sm5bf8 : Nat
1. ┌ fromJust#8vv2a5jnig : Text
2. └ fromJust#rrsqv1ogaq : Nat
3. fromJust#1o1iq26cq7 : Nat
3. fromJust#mkj3tehhkv : Nat
- 4. ns1.b : Nat
+ 5. ns2.b : Text
@ -408,8 +402,6 @@ unique type Y a b = Y a b
- 12. ns1.b : Nat
+ 13. ns2.b : Text
There were 1 auto-propagated updates.
Added definitions:
14. unique type Y a b
@ -491,7 +483,7 @@ bdependent = "banana"
Updates:
1. bdependent : Text
1. bdependent : Nat
2. bdependent : Text
@ -578,14 +570,14 @@ a = 555
New name conflicts:
1. a#ekguc9h648 : Nat
1. a#er8q007v02 : Nat
2. ┌ a#5f8uodgrtf : Nat
3. └ a#ekguc9h648 : Nat
2. ┌ a#75jrr0qj1c : Nat
3. └ a#er8q007v02 : Nat
Updates:
4. b#be9a2abbbg : Nat
4. b#j6aq9c9k9v : Nat
There were 1 auto-propagated updates.
@ -605,10 +597,10 @@ a = 555
New name conflicts:
1. a#8ss2r9gqe7 : Nat
1. a#nfb8lmj46i : Nat
2. ┌ a#5f8uodgrtf : Nat
3. └ a#ekguc9h648 : Nat
2. ┌ a#75jrr0qj1c : Nat
3. └ a#er8q007v02 : Nat
Updates:
@ -620,21 +612,21 @@ a = 555
.nsw> view a b
a#5f8uodgrtf : Nat
a#5f8uodgrtf = 555
a#75jrr0qj1c : Nat
a#75jrr0qj1c = 555
a#ekguc9h648 : Nat
a#ekguc9h648 = 444
a#er8q007v02 : Nat
a#er8q007v02 = 444
b#be9a2abbbg : Nat
b#be9a2abbbg =
b#j6aq9c9k9v : Nat
b#j6aq9c9k9v =
use Nat +
a#ekguc9h648 + 1
a#er8q007v02 + 1
b#kut4vstim7 : Nat
b#kut4vstim7 =
b#p50ctv8q17 : Nat
b#p50ctv8q17 =
use Nat +
a#5f8uodgrtf + 1
a#75jrr0qj1c + 1
```
```unison
@ -670,21 +662,21 @@ a = 777
.nsw> view a b
a#5f8uodgrtf : Nat
a#5f8uodgrtf = 555
a#75jrr0qj1c : Nat
a#75jrr0qj1c = 555
a#ekguc9h648 : Nat
a#ekguc9h648 = 444
a#er8q007v02 : Nat
a#er8q007v02 = 444
b#be9a2abbbg : Nat
b#be9a2abbbg =
b#j6aq9c9k9v : Nat
b#j6aq9c9k9v =
use Nat +
a#ekguc9h648 + 1
a#er8q007v02 + 1
b#kut4vstim7 : Nat
b#kut4vstim7 =
b#p50ctv8q17 : Nat
b#p50ctv8q17 =
use Nat +
a#5f8uodgrtf + 1
a#75jrr0qj1c + 1
```
##

View File

@ -497,6 +497,7 @@ But note it's not obvious how display should best be handling this. At the mome
.> display test2
Take a look at this:
foo : Nat -> Nat
foo n =
use Nat +
[: do the thing :]

View File

@ -7,11 +7,11 @@ Unison documentation is written in Unison. Documentation is a value of the follo
unique type builtin.Doc
= Join [builtin.Doc]
| Link Link
| Source Link
| Blob Text
| Signature Term
| Evaluate Term
| Blob Text
| Link Link
| Source Link
```
You can create these `Doc` values with ordinary code, or you can use the special syntax. A value of structural type `Doc` can be created via syntax like:
@ -147,12 +147,14 @@ Now that documentation is linked to the definition. We can view it if we like:
## Examples:
List.take.ex1 = builtin.List.take 0 [1, 2, 3, 4, 5]
List.take.ex1 : [Nat]
List.take.ex1 = builtin.List.take 0 [1, 2, 3, 4, 5]
🔽
ex1 = []
List.take.ex2 = builtin.List.take 2 [1, 2, 3, 4, 5]
List.take.ex2 : [Nat]
List.take.ex2 = builtin.List.take 2 [1, 2, 3, 4, 5]
🔽
ex2 = [1, 2]
@ -170,12 +172,14 @@ Or there's also a convenient function, `docs`, which shows the `Doc` values that
## Examples:
List.take.ex1 = builtin.List.take 0 [1, 2, 3, 4, 5]
List.take.ex1 : [Nat]
List.take.ex1 = builtin.List.take 0 [1, 2, 3, 4, 5]
🔽
ex1 = []
List.take.ex2 = builtin.List.take 2 [1, 2, 3, 4, 5]
List.take.ex2 : [Nat]
List.take.ex2 = builtin.List.take 2 [1, 2, 3, 4, 5]
🔽
ex2 = [1, 2]

View File

@ -64,7 +64,7 @@ Update
.> view.patch patch
Edited Terms: hey#8e79ctircj -> hey
Edited Terms: hey#ao70f78mjt -> hey
Tip: To remove entries from a patch, use
delete.term-replacement or delete.type-replacement, as
@ -72,7 +72,7 @@ Update
.> view.patch 1
Edited Terms: hey#8e79ctircj -> hey
Edited Terms: hey#ao70f78mjt -> hey
Tip: To remove entries from a patch, use
delete.term-replacement or delete.type-replacement, as

View File

@ -60,7 +60,7 @@ We used to have to know the full hash for a definition to be able to use the `re
.> names g
Term
Hash: #52addbrohu
Hash: #7pm9gkpflp
Names: g
.> replace f g
@ -70,12 +70,12 @@ We used to have to know the full hash for a definition to be able to use the `re
.> names g
Term
Hash: #52addbrohu
Hash: #7pm9gkpflp
Names: f g
.> view.patch
Edited Terms: f#msp7bv40rv -> f
Edited Terms: f#fs7la111vn -> f
Tip: To remove entries from a patch, use
delete.term-replacement or delete.type-replacement, as

View File

@ -104,10 +104,10 @@ Merge back into the ancestor.
New name conflicts:
1. p#a3ef1630bu : Text
1. p#ku52sq6ta7 : Text
2. ┌ p#a3ef1630bu : Text
3. └ p#fjqpdmdeqi : Text
2. ┌ p#ku52sq6ta7 : Text
3. └ p#p6cuhi6hb7 : Text
Tip: You can use `todo` to see if this generated any work to
do in this namespace and `test` to run the tests. Or you
@ -118,10 +118,10 @@ Merge back into the ancestor.
Resolved name conflicts:
1. ┌ y.a.p#a3ef1630bu : Text
2. └ y.a.p#fjqpdmdeqi : Text
1. ┌ y.a.p#ku52sq6ta7 : Text
2. └ y.a.p#p6cuhi6hb7 : Text
3. y.a.p#fjqpdmdeqi : Text
3. y.a.p#p6cuhi6hb7 : Text
Tip: You can use `undo` or `reflog` to undo this change.

View File

@ -4,10 +4,10 @@
go f i as acc =
_pattern = List.at i as
match _pattern with
None -> acc
Some _pattern1 ->
use Nat +
go f (i + 1) as (acc :+ f _pattern)
None -> acc
f a -> go f 0 a []
```

View File

@ -76,10 +76,10 @@ Let's do the update now, and verify that the definitions all look good and there
unique type A a b c d
= D d
| A a
| E a d
| B b
| C c
| E a d
| A a
structural type NeedsA a b
= NeedsA (A a b Nat Nat)

View File

@ -32,15 +32,15 @@ x = 4
.> links y
1. #kea5380m2n : #ffb7g9cull
1. #kvjtpqi06m : #pi9o52ongq
Tip: Try using `display 1` to display the first result or
`view 1` to view its source.
.> view 1
#kea5380m2n : #ffb7g9cull
#kea5380m2n = #ffb7g9cull#0
#kvjtpqi06m : #pi9o52ongq
#kvjtpqi06m = #pi9o52ongq#0
```
Well, it's hard to tell from those hashes, but those are right. We can confirm

View File

@ -101,9 +101,9 @@ We can look at the links we have:
```ucm
.> links coolFunction
1. coolFunction.license : License
1. coolFunction.doc : Doc
2. alice : Author
3. coolFunction.doc : Doc
3. coolFunction.license : License
Tip: Try using `display 1` to display the first result or
`view 1` to view its source.
@ -194,11 +194,11 @@ myLibrary.h x = x + 3
Note: The most recent namespace hash is immediately below this
message.
#l3kl2s1g8u
#noq1the6kh
#hcaq4np5kg (start of history)
#793qedilos (start of history)
.> unlink coolFunction.doc coolFunction

View File

@ -112,13 +112,13 @@ We can also delete the fork if we're done with it. (Don't worry, it's still in t
Note: The most recent namespace hash is immediately below this
message.
#4dmogr46d2
#979i457hd7
- Deletes:
feature1.y
#fe6mqhfcun
#kb0j8t02ue
+ Adds / updates:
@ -129,26 +129,26 @@ We can also delete the fork if we're done with it. (Don't worry, it's still in t
Original name New name(s)
feature1.y master.y
#qlrc4272pk
#bdvh2otcut
+ Adds / updates:
feature1.y
#mu2ju8e2ic
#kt38mg5bug
> Moves:
Original name New name
x master.x
#4adnodif8j
#gd173qpcn0
+ Adds / updates:
x
#ucb56c3fgj (start of history)
#hlflbqjqf9 (start of history)
```
To resurrect an old version of a namespace, you can learn its hash via the `history` command, then use `fork #namespacehash .newname`.

View File

@ -80,19 +80,19 @@ d = c + 10
New name conflicts:
1. c#0ja1qfpej6 : Nat
1. c#0t5t522gs3 : Nat
2. ┌ c#0ja1qfpej6 : Nat
3. └ c#jk19sm5bf8 : Nat
2. ┌ c#0t5t522gs3 : Nat
3. └ c#rrsqv1ogaq : Nat
4. d#gk1aqtfmh6 : Nat
4. d#libk4oh073 : Nat
5. ┌ d#gk1aqtfmh6 : Nat
6. └ d#qk9ub6bngd : Nat
5. ┌ d#libk4oh073 : Nat
6. └ d#qc2aihi6pd : Nat
Added definitions:
7. ┌ c#jk19sm5bf8 : Nat
7. ┌ c#rrsqv1ogaq : Nat
8. └ aaaa.tooManySegments : Nat
Tip: You can use `todo` to see if this generated any work to
@ -118,10 +118,10 @@ At this point, `a3` is conflicted for symbols `c` and `d`, but the original `a2`
a2.d : Nat
a2.d = a2.c + 10
a3.c#0ja1qfpej6 : Nat
a3.c#0ja1qfpej6 = 2
a3.c#0t5t522gs3 : Nat
a3.c#0t5t522gs3 = 2
a3.d#gk1aqtfmh6 : Nat
a3.d#gk1aqtfmh6 = c#0ja1qfpej6 + 10
a3.d#libk4oh073 : Nat
a3.d#libk4oh073 = c#0t5t522gs3 + 10
```

View File

@ -63,7 +63,7 @@ doc = cases
demure : [Nat] -> ()
doc : Nat -> ()
dopey : Char -> ()
grumpy : p4kl4dn7b41 -> ()
grumpy : q5g5surm1d1 -> ()
happy : Boolean -> ()
mouthy : [t] -> ()
pokey : [t] -> ()
@ -85,7 +85,7 @@ doc = cases
demure : [Nat] -> ()
doc : Nat -> ()
dopey : Char -> ()
grumpy : p4kl4dn7b41 -> ()
grumpy : q5g5surm1d1 -> ()
happy : Boolean -> ()
mouthy : [t] -> ()
pokey : [t] -> ()
@ -101,7 +101,7 @@ doc = cases
.> view grumpy
grumpy : p4kl4dn7b41 -> ()
grumpy : q5g5surm1d1 -> ()
grumpy = cases d -> ()
.> view happy

View File

@ -37,13 +37,13 @@ And then we add it.
.subpath> find.verbose
1. -- #v4a90flt15t54qnjbvbdtj42ouqo8dktu5da8g6q30l4frc6l81ttjtov42r1nbj5jq3hh98snlb64tkbb1mc5dk8les96v71b4qr6g
1. -- #ohtefitum4jai7d42hi6vc0vs8kupm9h81t1cspr9600r5grscm7jga452lnns29p7rkm9bq2u4o4ais0praq6r1uarbpfg4mf70758
unique type Foo
2. -- #v4a90flt15t54qnjbvbdtj42ouqo8dktu5da8g6q30l4frc6l81ttjtov42r1nbj5jq3hh98snlb64tkbb1mc5dk8les96v71b4qr6g#0
2. -- #ohtefitum4jai7d42hi6vc0vs8kupm9h81t1cspr9600r5grscm7jga452lnns29p7rkm9bq2u4o4ais0praq6r1uarbpfg4mf70758#0
Foo.Foo : Foo
3. -- #5k9rns49vrtujrpbiegajeja9qjjs77fju3usg1i1dpeo44kefkbce776u1kvqhvtutk6a6f178kovr422ocsd4fdsbsg7fprf4o0dg
3. -- #d9h62ubdj054t16h1mv5gc838ji23q8g5kgf35upp8f9ed9rq95pu2jg0lkq4c8k58p2c652o7mc2b7dr21b9m9jng512cop27sdo8o
fooToInt : Foo -> Int
@ -187,9 +187,9 @@ Cleaning up a bit...
Removed definitions:
1. unique type Foo
2. Foo.Bar : #i2nv821v0u
3. Foo.Foo : #i2nv821v0u
4. fooToInt : #i2nv821v0u -> Int
2. Foo.Bar : #8ei3pu3p2p
3. Foo.Foo : #8ei3pu3p2p
4. fooToInt : #8ei3pu3p2p -> Int
5. preserve.otherTerm : Optional baz -> Optional baz
6. preserve.someTerm : Optional x -> Optional x
7. patch patch

View File

@ -59,17 +59,17 @@ y = 2
most recent, along with the command that got us there. Try:
`fork 2 .old`
`fork #o7ncp4f3j1 .old` to make an old namespace
`fork #b9ghmnv7v4 .old` to make an old namespace
accessible again,
`reset-root #o7ncp4f3j1` to reset the root namespace and
`reset-root #b9ghmnv7v4` to reset the root namespace and
its history to that of the
specified namespace.
1. #nc81qsj2br : add
2. #o7ncp4f3j1 : add
3. #ucb56c3fgj : builtins.merge
4. #sjg2v58vn2 : (initial reflogged namespace)
1. #rggkaa5ori : add
2. #b9ghmnv7v4 : add
3. #hlflbqjqf9 : builtins.merge
4. #sg60bvjo91 : (initial reflogged namespace)
```
If we `reset-root` to its previous value, `y` disappears.

View File

@ -13,7 +13,7 @@ Let's look at some examples. We'll start with a namespace with just the builtins
#edu0qq546n (start of history)
#hfao0gunaf (start of history)
.> fork builtin builtin2
@ -42,21 +42,21 @@ Now suppose we `fork` a copy of builtin, then rename `Nat.+` to `frobnicate`, th
Note: The most recent namespace hash is immediately below this
message.
#u7d9er9k2f
#jnnhsl20gn
> Moves:
Original name New name
Nat.frobnicate Nat.+
#4dcjftvejg
#b61495giqo
> Moves:
Original name New name
Nat.+ Nat.frobnicate
#edu0qq546n (start of history)
#hfao0gunaf (start of history)
```
If we merge that back into `builtin`, we get that same chain of history:
@ -71,21 +71,21 @@ If we merge that back into `builtin`, we get that same chain of history:
Note: The most recent namespace hash is immediately below this
message.
#u7d9er9k2f
#jnnhsl20gn
> Moves:
Original name New name
Nat.frobnicate Nat.+
#4dcjftvejg
#b61495giqo
> Moves:
Original name New name
Nat.+ Nat.frobnicate
#edu0qq546n (start of history)
#hfao0gunaf (start of history)
```
Let's try again, but using a `merge.squash` (or just `squash`) instead. The history will be unchanged:
@ -106,7 +106,7 @@ Let's try again, but using a `merge.squash` (or just `squash`) instead. The hist
#edu0qq546n (start of history)
#hfao0gunaf (start of history)
```
The churn that happened in `mybuiltin` namespace ended up back in the same spot, so the squash merge of that namespace with our original namespace had no effect.
@ -191,47 +191,47 @@ At this point, Alice and Bob both have some history beyond what's in trunk:
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
.> history alice
Note: The most recent namespace hash is immediately below this
message.
#uollchacf2
#6q28310ueh
> Moves:
Original name New name
neatoFun productionReadyId
#7b6lii2lmc
#hkd9e8udkk
> Moves:
Original name New name
radNumber superRadNumber
#1l7bsgu3om
#oudl9oi8gt
+ Adds / updates:
bodaciousNumero neatoFun radNumber
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
.> history bob
Note: The most recent namespace hash is immediately below this
message.
#aicts31vr6
#9s1a1ak3fa
+ Adds / updates:
babyDon'tHurtMe no whatIsLove
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
```
Alice then squash merges into `trunk`, as does Bob. It's as if Alice and Bob both made their changes in one single commit.
@ -257,13 +257,13 @@ Alice then squash merges into `trunk`, as does Bob. It's as if Alice and Bob bot
Note: The most recent namespace hash is immediately below this
message.
#gjfd096e1s
#p7g0h14puu
+ Adds / updates:
bodaciousNumero productionReadyId superRadNumber
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
.> merge.squash bob trunk
@ -285,19 +285,19 @@ Alice then squash merges into `trunk`, as does Bob. It's as if Alice and Bob bot
Note: The most recent namespace hash is immediately below this
message.
#k7bfk3l7uv
#1i2d300kla
+ Adds / updates:
babyDon'tHurtMe no whatIsLove
#gjfd096e1s
#p7g0h14puu
+ Adds / updates:
bodaciousNumero productionReadyId superRadNumber
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
```
Since squash merges don't produce any merge nodes, we can `undo` a couple times to get back to our starting state:
@ -336,7 +336,7 @@ Since squash merges don't produce any merge nodes, we can `undo` a couple times
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
```
This time, we'll first squash Alice and Bob's changes together before squashing their combined changes into `trunk`. The resulting `trunk` will have just a single entry in it, combining both Alice and Bob's changes:
@ -380,14 +380,14 @@ This time, we'll first squash Alice and Bob's changes together before squashing
Note: The most recent namespace hash is immediately below this
message.
#ka70nifphh
#744kq5lo40
+ Adds / updates:
babyDon'tHurtMe bodaciousNumero no productionReadyId
superRadNumber whatIsLove
#hkrqt3tm05 (start of history)
#q9cdigs0bo (start of history)
```
So, there you have it. With squashing, you can control the granularity of your history.
@ -420,7 +420,7 @@ Another thing we can do is `squash` into an empty namespace. This effectively ma
#sui24env59 (start of history)
#qvt58h64so (start of history)
```
There's nothing really special here, `squash src dest` discards `src` history that comes after the LCA of `src` and `dest`, it's just that in the case of an empty namespace, that LCA is the beginning of time (the empty namespace), so all the history of `src` is discarded.
@ -485,13 +485,13 @@ This checks to see that squashing correctly preserves deletions:
Note: The most recent namespace hash is immediately below this
message.
#0kh907mpqb
#da2tmjvh5i
- Deletes:
Nat.* Nat.+
#edu0qq546n (start of history)
#hfao0gunaf (start of history)
```
Notice that `Nat.+` and `Nat.*` are deleted by the squash, and we see them deleted in one atomic step in the history.