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

Cannot put tests and Main in same file #3744

Closed
MikaelMayer opened this issue Mar 14, 2023 · 2 comments
Closed

Cannot put tests and Main in same file #3744

MikaelMayer opened this issue Mar 14, 2023 · 2 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking

Comments

@MikaelMayer
Copy link
Member

Dafny version

4.0.0

Code to produce this issue

method {:test} Test() {
}
method Main() {
}

Command to run and resulting output

> dafny run thefile.dfy
(no problem)

> dafny test thefile.dfy
(0,-1): Error: Duplicate member name: Main
1 resolution/type errors detected in thefile.dfy

What happened?

If I use {:main}, then the problem is also the same.

I should be able to run and test the file without compromise, like in Rust

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

Windows

@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking labels Mar 14, 2023
@davidcok
Copy link
Collaborator

Duplicate of #3369

@davidcok davidcok marked this as a duplicate of #3369 Mar 14, 2023
@MikaelMayer MikaelMayer self-assigned this Mar 21, 2023
@MikaelMayer MikaelMayer removed their assignment Apr 4, 2023
@davidcok
Copy link
Collaborator

davidcok commented Apr 4, 2023

Implemented in PR 3769. Duplicate of 3221

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 part: resolver Resolution and typechecking
Projects
None yet
Development

No branches or pull requests

2 participants