Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

delete.namespace does not assign to numberedArgs #1532

Open
Tracked by #4899
emiflake opened this issue May 6, 2020 · 0 comments
Open
Tracked by #4899

delete.namespace does not assign to numberedArgs #1532

emiflake opened this issue May 6, 2020 · 0 comments

Comments

@emiflake
Copy link

emiflake commented May 6, 2020

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

First, lets create two namespaces. foo and bar, and add some definitions.

x = 42
y = 100

  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

  ☝️  The namespace .foo is empty.

.foo> add

  ⍟ I've added these definitions:
  
    x : Nat
    y : Nat

z = x + y

  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

  ☝️  The namespace .bar is empty.

.bar> add

  ⍟ I've added these definitions:
  
    z : Nat

Let's see what we have created...

.> 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.

.> 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.

.> debug.numberedArgs

  1. .bar
  2. .builtin
  3. .foo

As you can see, the earlier output from `ls is still there.

Transcript source here:

delete-namespace-does-not-assign-numberedArgs.md.zip

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant