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.

[keyboardDrummer]

Using doo files is not easy or fast.

You can also pass project files to --library. On the CLI, this will automatically trigger building that library project into a doo file, and then use that doo file as if it had been passed to --library directly. I have to say though, this is an experimental feature and a critical part that I think is missing is caching of that automatically built .doo file. If you want to skip building the intermediate .doo file, you can use --dont-verify-dependencies. Currently you will still see output from the build of the intermediate doo, but I would be fine with only showing that if there are errors in it.

When passing a project file to --library, the IDE will not automatically build any .doo files, but consumes the library sources directly, which gives a faster development experience when editing both the consuming project and the library concurrently.

And this results in a warning about ... for every single file verified.

This PR #5827 should fix performance issues with passing many files to the Dafny CLI at once. If you only do a single invocation, you'll only see a single warning. I think doing multiple invocations for the same application is the root cause of you getting spammed with warnings.

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.

Errors and warnings that originate from verification will only be shown for the things you are verifying, while errors and warnings that originate from parsing and resolver will be shown for any file that occurs in your program, transitively included or passed to the CLI directly.

[seebees]

I think doing multiple invocations for the same application is the root cause of you getting spammed with warnings.

This may be true. The reason we verify each file individually is that the performance difference is huge. So my understanding is that you are saying that this has been fixed?

while errors and warnings that originate from parsing and resolver will be shown for any file that occurs in your program, transitively included or passed to the CLI directly.

First, are you suggesting that Warning: Could not find a trigger for this quantifier. is originating from the parsing/resolver? That error specifically seems to be coming from the verifier yes?

On the other hand, things like Warning: deprecated style: that I can 100% see as coming from parsing/resolver (yes?) I do not think is relevant if coming from a transitive source. I think that --library may offer a better experience today, but I don't think that such an message should be raised from transitive sources.

To jump to a slightly different place, I would never expect if I check for lint/formatting tool run on a file to follow the dependencies and tell me that some other file isn't formatted correctly.

But the big reason that I care, is that there are some warnings that can show up that are hugely important. Like assume without {:axiom} or {:only}. I want my build to 10000% fail on such things. But if I have to deal with all the transitive errors, this gets more complicated. Because it means I need all the dependencies to be fixed :)

So, while I might be able to move to --library someday, I would love to either have these kinds of errors never show up, or have some way to pick out the huge warnings and error on just these.

[keyboardDrummer]

So my understanding is that you are saying that this has been fixed?

I have made a fix that resolves memory leaks in the CLI invocation, which caused slowdowns when verifying large projects. I have tested that for 4.9, on one large Amazon internal project, doing a single invocation takes the same time as doing many small ones. However, the sample size of 1 is rather small so for Cryptools trying is the only way to find out.

First, are you suggesting that Warning: Could not find a trigger for this quantifier. is originating from the parsing/resolver? That error specifically seems to be coming from the verifier yes?

I believe that warning will also be shown if you do dafny resolve, so in that sense it comes from the resolver, even though it relates to verification. You could argue it should only be emitted for files that are also verified. I'd be willing to change that.

I do not think is relevant if coming from a transitive source

I rather not change the semantics of include statements at this point. I'm just about to mark them as deprecated. Without include statements, there's no more concept of transitive source. There'll only be source files and library files, and I'd be happy to hide warnings for library files.

I want my build to 10000% fail on such things. But if I have to deal with all the transitive errors, this gets more complicated. Because it means I need all the dependencies to be fixed :)

I get that, but I would rather help you to use --library than change the semantics of include directives. Maybe the next step is that I try out setting up project files in your codebase, testing that it performs well, and then ensure that you don't see warnings from library files.