{:compile false} has no effect on modules

[robin-aws]

Dafny version

4.3.0 (but has been true for a long time AFAICT)

Code to produce this issue

module {:compile false} PretendI'mNotHere {

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

Command to run and resulting output

% dafny run Scratch.dfy

Dafny program verifier finished with 0 verified, 0 errors
BOO

What happened?

According to the reference manual {:compile false} should apply to "any top-level declaration". There are even test cases in the integration suite that seem to believe the attribute should work on modules, but AFAICT no test actually verifies no code is outputted.

This is especially an issue for externs in Go (and likely Python as well), since examples like comp/Extern.dfy only work because passing the extra Extern.go file on the CLI causes it to overwrite the incorrectly Dafny-generated Extern.go file.

Although I'm a bit worried about just fixing this, since there may be code out there using {:compile false} on modules anyway, it seems like no longer emitting code as directed is extremely likely to break loudly.

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

Mac