"Dafny > Dafny tests" not working with project files

[MikaelMayer]

I have a project file like this:

dfyconfig.toml
Source/
  myincludedFile.dfy
  myfile.dfy

and myfile.dfy contains

module TestModule {
  import opened ImportedModule
  method {:test} OneTest() {
    expect true;
  }
}

whereas myincludedFile.dfy contains (to simplify)

module ImportedModule {
}

myfile.dfy is open in my VSCode editor, I right-click, and click on Dafny > Dafny test. It launches a command line that fails:

& dafny.exe test --no-verify "...\Source\Dafny-compiler-rust-path-simplification.dfy"

which fails with the issue:

myincludedFile.dfy(4,16): Error
: module ImportedModule does not exist
  |
4 |   import opened ImportedModule

Potential solutions, in preference order:

• Display a clickable Run button in the gutter to run each test individually or all the test of the module (like Rust)
• Fix this command so that it would run all the tests of dfyconfig.toml but filter those in this file?
• Fix this command by running all the tests on "dfyconfig.toml" because & dafny.exe test --no-verify "...\dfyconfig.toml" should work (but it does not in my case because of missing assembly references)

[keyboardDrummer]

Fix this command so that it would run all the tests of dfyconfig.toml but filter those in this file?

That seems simplest, since we have a --find-project option now. We would still need to add something like --filter-position for dafny test though.

[MikaelMayer]

I hit the same issue with @erniecohen while trying to run a simple program with a dfyconfig.toml

Program:

trait X {}

datatype C<T extends X> extends X = C(t: T)

method Main() {
  print "Hello\n";
}

dfyconfig.toml:

[options]
general-traits = "datatype"
type-system-refresh = true
general-newtypes = true

Right-click on the program, "dafny build", "dafny run" and "dafny test" won't work.
On the dfyconfig.toml, there is Dafny menu either.