Clean up the transcript and see that it passes

The issue had already been fixed at some point.

Closes #1532.
This commit is contained in:
Greg Pfeil 2024-06-03 11:56:33 -06:00
parent 2bf53bc3ae
commit 811c9e70bb
No known key found for this signature in database
GPG Key ID: 1193ACD196ED61F2
2 changed files with 109 additions and 79 deletions

View File

@ -1,99 +1,40 @@
When using `delete.namespace` ucm will not assign `numberedArgs` which is unexpected.
It also assigns multiple things to the same number (possibly related).
## Transcript showing the problem
```ucm
.> builtins.merge
```
First, lets create two namespaces. `foo` and `bar`, and add some definitions.
```unison
x = 42
y = 100
foo.x = 42
foo.y = 100
bar.z = x + y
```
```ucm
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`:
x : Nat
y : Nat
```
```ucm
☝️ The namespace .foo is empty.
.foo> add
⍟ I've added these definitions:
x : Nat
y : Nat
```
```unison
z = x + y
.> add
```
```ucm
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`:
z : Nat
```
```ucm
☝️ The namespace .bar is empty.
.bar> add
⍟ I've added these definitions:
z : Nat
```
Let's see what we have created...
```ucm
.> ls
1. bar/ (1 definition)
2. builtin/ (168 definitions)
3. foo/ (2 definitions)
```
Now, if we try deleting the namespace `foo`, we get an error, as expected.
```ucm
```ucm:error
.> delete.namespace foo
⚠️
I couldn't delete
1. foo.x : builtin.Nat
2. foo.y : builtin.Nat
because it's still being used by these definitions:
1. bar.z : builtin.Nat
```
However, the numbered arguments are not assigned by that command.
Any numbered arguments should refer to `bar.z`.
```ucm
.> debug.numberedArgs
1. .bar
2. .builtin
3. .foo
```
As you can see, the earlier output from `ls is still there.
We can then delete the dependent term, and then delete `foo`.
```ucm
.> delete.term 1
.> delete.namespace foo
```

View File

@ -0,0 +1,89 @@
```ucm
.> builtins.merge
Done.
```
First, lets create two namespaces. `foo` and `bar`, and add some definitions.
```unison
foo.x = 42
foo.y = 100
bar.z = x + 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`:
bar.z : Nat
foo.x : Nat
foo.y : Nat
```
```ucm
.> add
⍟ I've added these definitions:
bar.z : Nat
foo.x : Nat
foo.y : Nat
```
Let's see what we have created...
```ucm
.> ls
1. bar/ (1 term)
2. builtin/ (469 terms, 74 types)
3. foo/ (2 terms)
```
Now, if we try deleting the namespace `foo`, we get an error, as expected.
```ucm
.> delete.namespace foo
⚠️
I didn't delete the namespace because the following
definitions are still in use.
Dependency Referenced In
x 1. bar.z
y 2. bar.z
If you want to proceed anyways and leave those definitions
without names, use delete.namespace.force
```
Any numbered arguments should refer to `bar.z`.
```ucm
.> debug.numberedArgs
1. bar.z
2. bar.z
```
We can then delete the dependent term, and then delete `foo`.
```ucm
.> delete.term 1
Done.
.> delete.namespace foo
Done.
```