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

IDE may be loading Std library twice #456

Open
markrtuttle opened this issue Dec 10, 2023 · 1 comment
Open

IDE may be loading Std library twice #456

markrtuttle opened this issue Dec 10, 2023 · 1 comment

Comments

@markrtuttle
Copy link

The IDE complains "Duplicate module name: FileIOParser" if I load a project containing the following two files that use the new Std standard libraries. Reproduce this error using the attached tar file example.tar.gz.

test.dfy

module Test {
  import opened Std.Wrappers
  function count(i: int): Option<int> {
    if i < 0 then None else Some(i+1)
  }
}

dfyconfig.toml

[options]
standard-libraries = true

Run code . in the enclosing directory using a recent dafny nightly (nightly-2023-12-10-4faa561) and open the file test.dfy. The extension will resolve and verify the file as expected. Type a space anywhere in the file. The extension will start resolution and report "Resolution Failed" and point to the first like of the dfyconfig.toml file. The error message will be

Files referenced by project are:
test.dfy
DafnyStandardLibraries-notarget.dfy
DafnyStandardLibraries-notarget.dfy
DafnyStandardLibraries.dfyParser

the referenced file DafnyStandardLibraries-notarget.dfy contains error(s) but is not owned by this project. The first error is:
Duplicate module name: FileIOParser

Run "Restart Dafny" and the file will verify successfully as before. Repeat...

@markrtuttle
Copy link
Author

markrtuttle commented Dec 11, 2023

Similar to Dafny issue dafny-lang/dafny#4858 and possibly fixed by pull request dafny-lang/dafny#4861 fixing the language server.

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