Warnings raised from

[seebees]

Dafny version

4.8.0

Code to produce this issue

include "module_with_warning.dfy"
module Foo {
  import ModuleWithWarning
}

Command to run and resulting output

Warnings from included file

What happened?

Not see warnings. I only want to see the errors/warnings et al from the file I'm verifying not all my transitive dependencies.

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

Linux, Mac

[keyboardDrummer]

Could you indicate what you're doing to run into this issue? I see source code but not a particular command that you're running. My best guess is that you're using the Dafny IDE but I'd rather not guess.

[keyboardDrummer]

In any case, an include is considered part of your sources, so I would expect any warnings from them to be shown when passing the including file to Dafny.

In the case where you have a library, if you compile the library into a .doo file and include that in another dafny invocation, then you should not see warnings from the doo file.

However, if you want to create the doo file when warnings are present, you will have to use the option --allow-warnings otherwise the build will fail, and this option will be recorded in the doo file. Any project consuming that doo file will fail to build unless it also uses --allow-warnings, even if the sources of that project have no warnings.

[seebees]

The problem is that I have a very complicated build pipeline. Using doo files is not easy or fast.

Here is an example:
https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/11293823325/job/31412935381#step:9:29

You can see that we are running the following command:

find . -name '*.dfy' | xargs -n 1 -P 5 -I % dafny verify \
		--cores 2 \
		--unicode-char false \
		--function-syntax 3 \
		--log-format csv \
		--verification-time-limit 100 \
		--resource-limit 90000000 \
		--allow-warnings --allow-external-contracts \
		%

And this results in a warning about /Users/runner/work/aws-cryptographic-material-providers-library/aws-cryptographic-material-providers-library/libraries/src/NonlinearArithmetic/DivMod.dfy(1208,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. for every single file verified.

The above command will never verify libraries/src/NonlinearArithmetic/DivMod.dfy directly. This file is included transitively however.

If I give Dafny a single file to verify, and ask Dafny to verify the whole program. i.e. this file and all the transitive includes. Then I would expect to see warnings on all transitive files as well. However, I would expect the warnings to work the same way verification works. If I'm only asking to verify foo.dfy then I would expect to only see verification failures and warnings about foo.dfy not everything.