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

Resolution fails when using a symbol from a default export set of an inner module #4328

Closed
keyboardDrummer opened this issue Jul 24, 2023 · 0 comments · Fixed by #4329
Closed
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Jul 24, 2023

Dafny version

4.2

Code to produce this issue

In the Dafny IDE, not on the CLI, use the following code, and it will show you an error where it should not:

module Outer {
  method Bar() {
    Inner.Foo(); // unresolved identifier: Foo
  }
}

module Outer.Inner {
    export provides Foo
    method Foo() { }
}

What type of operating system are you experiencing the problem on?

Mac

@keyboardDrummer keyboardDrummer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Jul 24, 2023
@keyboardDrummer keyboardDrummer self-assigned this Jul 24, 2023
@keyboardDrummer keyboardDrummer changed the title Module resolution fails when using import opened on an inner module with an export set Module resolution fails when using a default export set of an inner module Jul 24, 2023
@keyboardDrummer keyboardDrummer changed the title Module resolution fails when using a default export set of an inner module Resolution fails when using a default export set of an inner module Jul 24, 2023
@keyboardDrummer keyboardDrummer changed the title Resolution fails when using a default export set of an inner module Resolution fails when using a symbol from a default export set of an inner module Jul 24, 2023
keyboardDrummer added a commit that referenced this issue Jul 24, 2023
Fixes #4328

### Changes
Fix clone method of ModuleExportDecl

### Testing
No tests added.

Instead, we should run part of the testsuite using the IDE instead of
the CLI, since the IDE runs additional code (caching code, which
currently uses cloning, which isn't tested well)

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer added a commit to keyboardDrummer/dafny that referenced this issue Sep 15, 2023
Fixes dafny-lang#4328

### Changes
Fix clone method of ModuleExportDecl

### Testing
No tests added.

Instead, we should run part of the testsuite using the IDE instead of
the CLI, since the IDE runs additional code (caching code, which
currently uses cloning, which isn't tested well)

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant