parent modules break verification when included through project files

[erniecohen]

Dafny version

4.6.0 (nightly 4/17)

Code to produce this issue

With the following files (all in the same directory), the dafny server fails on b.dfy.
(building the dfyconfig file works)

a.dfy: a {}
b.dfy: module a.b { method test() { assert true; }}
dfyconfig.toml: includes = ["*.dfy"]

Command to run and resulting output

No response

What happened?

verification should succeed.
more generally, there should be uniformity between the CLI and the Dafny server.

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

Mac

[keyboardDrummer]

A workaround for this problem is to declare nested modules in the same file as their parent module

[erniecohen]

That workaround doesn't work so well when you have lots of nested modules (e.g., when they represent various implementations of an interface).

The workaround I've been using for module foo is to keep foo.dfy in the same folder, and to also add into the foo directory a dfyconfig.toml file of the form

base = "../dfyconfig.toml"
excludes = ["foo.dfy"]

This hides foo.dfy when building files under foo, while allowing foo.dfy (and all of the other files in the foo hierarchy) to be used by all modules that do not descend from foo.