Rework warn-as-error option #4971

keyboardDrummer · 2024-01-10T11:35:57Z

The existing option --warn-as-error causes everything that would otherwise be a warning, to be recorded as an error. Because the Dafny compiler often uses the presence of errors to determine whether to continue, using --warn-as-error causes compilation to potentially halt earlier when it's turned on. This can hide errors until warnings that occur earlier in the pipeline have been resolved. In addition, using this option makes it impossible for the user to see what was originally a warning instead of an error.

Changes

Replace the option --warn-as-error with the option --succeed-on-warnings. Besides having the opposite meaning, this option no longer turns warnings into errors, nor does it reduce the amount of diagnostics collected in compilation. When turned off, the default, any warnings will cause the CLI to return an error exit code and prevent the execution of the Dafny code. All forms of execution, whether directly executing it or through the creation of build artifacts such as generated code (cs/java/go/etc) or further compiled generated code (dll/jar/etc), are prevented.
A doo file that was created using --succeed-on-warnings causes a warning if used by a consumer that does not use it.
Change the behavior of --warn-deprecation=false so that deprecation diagnostics are reported as information, which means they show up in the IDE
Flip the behavior of --warn-deprecation and change the name to --allow-deprecation, so the default is now false, which is common for boolean options. It's slightly nicer for user to type --allow-deprecation instead of --warn-deprecation=false.

Caveats

When a user is developing and wants to quickly run their code to test something, but the code has warnings, the user must add --succeed-on-warnings to their dafny run invocation.
This change is not backwards compatible.
- Dafny users must remove any usages of --warn-as-error
- If users have builds that were passing with warnings, they have to add --succeed-on-warnings to allow them to still pass
- If users upgrade to a new Dafny version, and are not using --succeed-on-warnings, and do not want to migrate off of deprecated feature, they will have to use --allow-deprecation. In the future we will introduce dafny migrate to enable use to automatically move off of deprecated features, allowing them to instantly upgrade to newer Dafny versions without having to use --allow-deprecation or --succeed-on-warnings.
- Any instance of --warn-deprecation false must be replaced with --allow-deprecation

How has this been tested?

Updated tests

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…o stopOnWarnings

robin-aws · 2024-01-10T16:19:36Z

Just commenting on the description rather than the implementation.

I'm definitely in favour of no longer converting warnings to errors and instead having the option to fail on warnings.

I don't think it makes sense to fail on warnings by default though. IMO the whole point of a "warning" as opposed to an "error" is that it isn't fatal by default, and if we have warnings that should fail the pipeline by default we should upgrade them to errors with ways to quickly fix/suppress them if necessary.

I suspect based on other conversations that the underlying reason for wanting this is that Dafny currently has things it only conditionally flags as errors based on command, which we want to make warnings instead. For example, assume statements without {:axiom} or methods without bodies: those are allowed by dafny verify but errors in dafny translate. The problem with making those warnings is they will be just noise when using Dafny as a proof assistant and never translating or executing the code.

I'd suggest we try to tackle supporting these different use cases better more directly instead. Perhaps there should be a project file property indicating whether the Dafny code will only be used for verification and not execution, similar to the <OutputType> property in .csproj files that can be Exe or Library and so on. That way if a project was tagged as "executable", dafny verify could produce errors during resolution if it finds execution issues such as methods without bodies.

keyboardDrummer · 2024-01-10T17:04:58Z

I don't think it makes sense to fail on warnings by default though. IMO the whole point of a "warning" as opposed to an "error" is that it isn't fatal by default, and if we have warnings that should fail the pipeline by default we should upgrade them to errors with ways to quickly fix/suppress them if necessary.

It's unclear to me how you are positioning warnings. It sounds to me like you're saying warnings are never fatal, which implies that they are allowed to proliferate in a codebase, which I think makes them more annoying than useful.

I would like to position a warning as something that is fatal by default in CI, but not fatal during development.

With this PR, warnings are effectively not fatal during development. You run Dafny code during development by calling dafny run --pass-on-warnings. If you are calling dafny verify during development, you likely don't care about the exit code and you have no need to use --pass-on-warnings. Also, if you are using dafny server, there is no relevant exit code and you don't need --pass-on-warnings.

I have considered letting dafny run have --pass-on-warnings=true by default, since I believe dafny run is mostly used during development. However, I want to be defensive and not make that change, because I can also imagine a future where dafny run is used for production purposes, and for example there is a dafny debug that's meant for development.

I suspect based on other conversations that the underlying reason for wanting this is that Dafny currently has things it only conditionally flags as errors based on command, which we want to make warnings instead. For example, assume statements without {:axiom} or methods without bodies: those are allowed by dafny verify but errors in dafny translate.

The problem with making those warnings is they will be just noise when using Dafny as a proof assistant and never translating or executing the code.

I disagree. I think even as a proof assistant you want to differentiate between an assume that you are adding temporarily as part of developing your proof, and one that you are checking into your codebase for the long term: assume {:axiom}. I think this is unrelated to whether you're also executing code.

robin-aws · 2024-01-10T17:32:55Z

Okay I get where you're coming from: you want all warnings to always block committing changes to a project. I don't think that's the only valid definition of "warning" but I do like the idea of being that strict about it. Really it makes warnings "non-fatal errors" - ones that ultimately mean the program isn't valid but that don't block doing useful local development with it such as executing it.

If we're going that route though, I think we should review all our warnings to look for ones that shouldn't block CI before we make failing on warnings the default. There are definitely ones that should not be interpreted as "non-fatal errors" and aren't necessarily quick to address. For example: "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead". Similarly, although I think it's reasonable to make assume without {:axiom} a warning, we shouldn't do the same for things that are only errors for translation/execution like bodiless methods (and it's possible my suggestion for catching those errors by communicating the intent of a project might be useful orthogonally).

It might also be to have more severity levels: "warning" for things that may or may not be issues, "error" for definite problems that shouldn't be allowed in CI but don't block development, and "fatal" for things where the pipeline can't proceed any further.

robin-aws · 2024-01-10T19:14:12Z

Minor quibble: I'd suggest --fail-on-warnings:false instead of --pass-on-warnings for pure readability, just because "fail" feels a little more intuitive in the context of CLI exit codes. Or perhaps --succeed-on-warnings?

keyboardDrummer · 2024-01-11T09:29:21Z

I think we should review all our warnings to look for ones that shouldn't block CI before we make failing on warnings the default

What do you think is missing from the test-suite to complete that review?

For example: "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead"

One change that I forgot to list in the PR details is that the option --warn-deprecation is off by default, and that deprecation diagnostics are reported as "information" when this option is turned off, meaning they still show up in the IDE.

Similarly, although I think it's reasonable to make assume without {:axiom} a warning, we shouldn't do the same for things that are only errors for translation/execution like bodiless methods

I think we should let these two behave the same, so a bodyless method will produce a warning whether you are executing or not, unless you annotate it with {:axiom}, similar to an assume statement.

It might also be to have more severity levels: "warning" for things that may or may not be issues, "error" for definite problems that shouldn't be allowed in CI but don't block development, and "fatal" for things where the pipeline can't proceed any further.

I'm not sure I understand what you're suggesting. The labels we have at our disposal through LSP are "error", "warning" and "information". I think the common way to map these to behavior are:
"error" => always returns an error exit code
"warning" => returns an error exit code depending on CLI options
"information" => never returns an error exit code

Minor quibble: I'd suggest --fail-on-warnings:false instead of --pass-on-warnings for pure readability, just because "fail" feels a little more intuitive in the context of CLI exit codes. Or perhaps --succeed-on-warnings

It's nicer for boolean options to have false be the default, so you can turn them on using just --option-name, but I agree --fail-on-warnings is an easier to understand name. If --succeed-on-warnings is clearer than --pass.. to you, then I'd prefer that.

robin-aws · 2024-01-12T04:15:53Z

I think we should review all our warnings to look for ones that shouldn't block CI before we make failing on warnings the default

What do you think is missing from the test-suite to complete that review?

I did a quick scan myself - I just wanted to check for any warnings that were obviously unreasonable to block on, and the point about not warning on deprecation any more helps.

The only one that gave me pause was the one in DafnyProject about the IDE only recognizing files named dfyconfig.toml. I'm surprised that one didn't cause a test failure.

Similarly, although I think it's reasonable to make assume without {:axiom} a warning, we shouldn't do the same for things that are only errors for translation/execution like bodiless methods

I think we should let these two behave the same, so a bodyless method will produce a warning whether you are executing or not, unless you annotate it with {:axiom}, similar to an assume statement.

Ah fair enough, having to add {:axiom} is a reasonable way to suppress that one.

It might also be to have more severity levels: "warning" for things that may or may not be issues, "error" for definite problems that shouldn't be allowed in CI but don't block development, and "fatal" for things where the pipeline can't proceed any further.

I'm not sure I understand what you're suggesting. The labels we have at our disposal through LSP are "error", "warning" and "information". I think the common way to map these to behavior are: "error" => always returns an error exit code "warning" => returns an error exit code depending on CLI options "information" => never returns an error exit code

Damn, didn't realize the LSP was prescriptive about that, never mind.

Minor quibble: I'd suggest --fail-on-warnings:false instead of --pass-on-warnings for pure readability, just because "fail" feels a little more intuitive in the context of CLI exit codes. Or perhaps --succeed-on-warnings

It's nicer for boolean options to have false be the default, so you can turn them on using just --option-name, but I agree --fail-on-warnings is an easier to understand name. If --succeed-on-warnings is clearer than --pass.. to you, then I'd prefer that.

Sure, let's go with --succeed-on-warnings then!

…o stopOnWarnings

robin-aws

Implementation looks great, just asking for a couple of tweaks.

I did realize that --succeed-on-warnings will be confusing for dafny run and dafny test, since it's only the pipeline that is "succeeding" and not the process' exit code. I suggest --allow-warnings instead, assuming it's just an easy search-and-replace.

robin-aws · 2024-02-08T18:07:51Z

Source/DafnyCore/Compilers/CSharp/Synthesizer-Csharp.cs

@@ -179,11 +179,12 @@ public class CsharpSynthesizer {
    var methodName = method.GetCompileName(Options);

    if (((Function)method).Ens.Count != 0) {
-      compiler.Error(CompilerErrors.ErrorId.c_possibly_unsatisfied_postconditions, lastSynthesizedMethod.tok,


I'd be happier if this stayed as an error, does it have to change?

Previously errors did not block code from being generated. A current test is hitting this line but still generating tests and running those. This is the test: https://github.com/dafny-lang/dafny/blob/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.dfy#L5

You can see it expects
// CHECK: .*Error: Post-conditions on function Identity might be unsatisfied when synthesizing code for method mockUnsafe.*
but also expects the test runner to run:
// CHECK: .*_module.__default.FailingTestUsingMock.*

With this PR, errors block code from being generated (see the changes here and here). Previously, errors would block code from being downstream compiled and run, but code could still be emitted.

Because of errors being more blocking, the line you commented on needs to be a warning and the TestAttribute tests needs --succeed-on-warnings, for it to still run. I think effect of this PR is more restrictive when it comes to hitting this line, because the test needs an extra flag before it passes, so it's an improvement. Whether you want this line to be an error and update TestAttribute.dfy, I don't now but I'd leave that for another PR.

Got it. I don't love downgrading the severity of the issue but we should still support the use case. I cut #5075 for follow up instead.

robin-aws · 2024-02-08T18:09:54Z

Source/DafnyCore/DafnyOptions.cs

@@ -720,7 +720,7 @@ public enum IncludesModes {
          }

        case "warningsAsErrors":


The release notes should mention that /warningsAsErrors is changing behavior too.

robin-aws · 2024-02-08T18:16:52Z

Source/DafnyCore/DooFile.cs

+  public static bool OptionValuesImplied(Option option, object first, object second) {
+    try {
+      return !(bool)first || (bool)second;
+    } catch (NullReferenceException) {


I'd prefer not to swallow this as it shouldn't happen with released Dafny versions: AFAICT you can only be missing options in doo files if they were built with an older version of Dafny, which is explicitly blocked.

Note that I return false here, so it will prevent the doo file from being used.

It also sounds like you're saying that you'd like a version check when using Doo files, and that it's currently not there, otherwise I wouldn't have been able to hit this exception.

No the version check totally exists! https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/DooFile.cs#L129-L133. I think we're missing an integration test for that though - I recall writing one that depended on checking in a doo file with an older version, but I think we had to pull it out for some reason.

However that only kicks in when we bump the Dafny version number, which we usually don't do until just before releasing. So it's not hard to hit the NRE in development if you change the set of recorded options and have doo files lying around from before the change.

It might be worth defensively emitting a clearer error message, even if this would be an internal error that shouldn't happen on released Dafny versions. But I definitely don't want to silently return false since it would indicate something else has gone wrong.

It might be worth defensively emitting a clearer error message, even if this would be an internal error that shouldn't happen on released Dafny versions. But I definitely don't want to silently return false since it would indicate something else has gone wrong.

I think I disagree, but I've made the change you suggested.

robin-aws · 2024-02-08T18:19:29Z

Source/DafnyDriver/DafnyBackwardsCompatibleCli.cs

@@ -11,7 +11,7 @@ namespace Microsoft.Dafny;
 public interface ILegacyParseArguments { }

 // TODO: Refactor so that non-errors (NOT_VERIFIED, DONT_PROCESS_FILES) don't result in non-zero exit codes
-public enum ExitValue { SUCCESS = 0, PREPROCESSING_ERROR, DAFNY_ERROR, COMPILE_ERROR, VERIFICATION_ERROR, FORMAT_ERROR }
+public enum ExitValue { SUCCESS = 0, PREPROCESSING_ERROR = 1, DAFNY_ERROR = 2, COMPILE_ERROR = 3, VERIFICATION_ERROR = 4, FORMAT_ERROR = 5 }


Ah does C# not guarantee this indexing by default?

It does, but sometimes you have to know what the numbers are when looking at test output, so I found this easier to read. Also, I think when you're casting enums to numbers and exposing those numbers to your clients, it's better to set them explicitly, so they don't accidentally change when adding a new enum member in the middle.

robin-aws · 2024-02-08T18:21:41Z

Source/DafnyRuntime/DafnyRuntimeGo/System_/System_.go

What happened here? it looks like goimports didn't get applied, but CI should be catching the mismatch.

O is this when it does not get applied? I couldn't judge by the changes. It looked to me like it was now suddenly applying the formatting :-D but apparently goimports really likes indentation.

Made a change so this gets reverted.

robin-aws · 2024-02-08T18:23:59Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/arrays.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false


Why this change?

Just cleanup. The test does not need that option.

robin-aws · 2024-02-08T18:26:12Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151-more.dfy.expect

@@ -6,19 +6,15 @@ git-issue-1151-more.dfy(13,5): Error: Abstract type ('_module.Opaque') cannot be

 Dafny program verifier did not attempt verification
 git-issue-1151-more.dfy(13,5): Error: Abstract type ('_module.Opaque') cannot be compiled; perhaps make it a type synonym or use :extern.
-Wrote textual form of partial target program to git-issue-1151-more-java/git_issue_1151_more.java


Was it intentional to lose these outputs?

Yes. I decided in this PR that it's dangerous to generate target code when the Dafny compiler emits errors. Previously translation errors would only block downstream compilation and running.

A side-effect is that these partial target programs are no longer emitted. I think that partially translated programs are only useful for debugging the Dafny language, so I'm OK to lose that feature now and if someone needs it they can add a hidden developer option for it.

Completely agree with that and was tempted to do this myself in the past, just didn't spot the connection - thanks for that change then!

robin-aws · 2024-02-08T18:28:20Z

docs/dev/news/4971.feat

+- Flip the behavior of `--warn-deprecation` and change the name to `--allow-deprecation`, so the default is now false, which is standard for boolean options.
+- When using `--allow-deprecation`, deprecated code is shown using tooltips in the IDE, and on the CLI when using `--show-tooltips`.
+- Replace the option `--warn-as-error` with the option `--succeed-on-warnings`. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous `--warn-as-error` option, warnings are always reported as warnings.
+  - During development, users must use `dafny run --succeed-on-warnings` if they want to run their Dafny code when it contains warnings.


This is worth mentioning in the user guide as well somewhere.

…o stopOnWarnings

robin-aws · 2024-02-12T17:08:46Z

docs/DafnyRef/UserGuide.md

@@ -233,7 +233,7 @@ implementation.

 The options relevant to this command are
 - those relevant to the command-line itself
-   - `--warn-as-errors` --- turn all warnings into errors, which alters [dafny's exit code](#sec-exit-codes)
+   - `--allow-warnings` --- return a success [exit code](#sec-exit-codes), even when there are warnings 


~~Not true though since dafny run or dafny test still could return a non-zero exit code.~~

Edit: missed that this was specific to dafny resolve, disregard

keyboardDrummer added 3 commits January 10, 2024 11:28

First step in introducing stop-on-warnings and continue-on-warnings

1c25610

Listen to fail and pass on warnings options

8929611

Refactoring

25f63e1

keyboardDrummer requested a review from robin-aws January 10, 2024 11:35

keyboardDrummer changed the title ~~Fail on warnings~~ Pass on warnings Jan 10, 2024

keyboardDrummer changed the title ~~Pass on warnings~~ Rework warn-as-error option Jan 10, 2024

Updates

3a52d6c

keyboardDrummer mentioned this pull request Jan 10, 2024

Standard Library fails to build to target:lib (doo) #4964

Closed

keyboardDrummer added 3 commits January 10, 2024 14:59

Merge remote-tracking branch 'origin/master' into stopOnWarnings

ab8e162

Do not emit compilation artifacts if failing compilation

69e95d9

Ran formatter

1d59e4d

keyboardDrummer mentioned this pull request Jan 10, 2024

Axiom warnings #3553

Merged

keyboardDrummer added 3 commits January 10, 2024 15:29

FixeS

5d6fe4e

Fix test

3e20f09

Merge branch 'stopOnWarnings' of github.com:keyboardDrummer/dafny int…

e7aed56

…o stopOnWarnings

keyboardDrummer added 9 commits January 12, 2024 17:13

Update tests

2bba364

Updates

e4f26e4

Merge branch 'master' into stopOnWarnings

7caee01

update name

88e0e9c

Merge branch 'stopOnWarnings' of github.com:keyboardDrummer/dafny int…

5b3b840

…o stopOnWarnings

Trigger CI

31c66c0

Fix issues

92c61eb

Fix exit value

2b8f858

Fixes

e288e3a

keyboardDrummer added 10 commits February 1, 2024 14:42

Fix merge booboo

f4a5797

Fix tests

9181c74

Fix tests

649c9f4

Merge branch 'stopOnWarnings' of github.com:keyboardDrummer/dafny int…

792414a

…o stopOnWarnings

Fixes for TestAttribute.dfy

bd65ca5

Remove warn-as-errors references

c8a2803

Update standard library doo files

696515c

Update runtime file

6d4aab9

Update go runtime

b3bfa85

Merge branch 'master' into stopOnWarnings

e9009c6

keyboardDrummer enabled auto-merge (squash) February 2, 2024 10:11

robin-aws requested changes Feb 8, 2024

View reviewed changes

keyboardDrummer added 5 commits February 9, 2024 12:26

Code review

ecb80cf

Add documentation update

130b37e

Rename --succeed-on-warnings to --allow-warnings

e7c205d

Update description

9b0476d

Merge branch 'master' into stopOnWarnings

ab91581

keyboardDrummer requested a review from robin-aws February 9, 2024 11:50

keyboardDrummer added 3 commits February 9, 2024 16:57

Update stdlib doo files

407e599

Ran formatter

e4baa39

Merge branch 'stopOnWarnings' of github.com:keyboardDrummer/dafny int…

0b1992d

…o stopOnWarnings

robin-aws mentioned this pull request Feb 9, 2024

{:synthesize} failures don't block executing programs #5075

Open

keyboardDrummer added 2 commits February 12, 2024 12:47

Update doo files

784693a

Updated return false to throwing exception

fabf81e

robin-aws reviewed Feb 12, 2024

View reviewed changes

robin-aws approved these changes Feb 12, 2024

View reviewed changes

Merge branch 'master' into stopOnWarnings

5817ea1

keyboardDrummer merged commit 2688c9b into dafny-lang:master Feb 12, 2024

keyboardDrummer deleted the stopOnWarnings branch February 12, 2024 18:13

RustanLeino mentioned this pull request Apr 24, 2024

{:only} causes crash #5064

Closed

		@@ -720,7 +720,7 @@ public enum IncludesModes {
		}

		case "warningsAsErrors":

		@@ -1,4 +1,4 @@
		// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment --spill-translation --unicode-char:false

Rework warn-as-error option #4971

Rework warn-as-error option #4971

Uh oh!

Conversation

keyboardDrummer commented Jan 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Caveats

How has this been tested?

Uh oh!

robin-aws commented Jan 10, 2024

Uh oh!

keyboardDrummer commented Jan 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robin-aws commented Jan 10, 2024

Uh oh!

robin-aws commented Jan 10, 2024

Uh oh!

keyboardDrummer commented Jan 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robin-aws commented Jan 12, 2024

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Feb 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robin-aws Feb 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

keyboardDrummer commented Jan 10, 2024 •

edited

Loading

keyboardDrummer commented Jan 10, 2024 •

edited

Loading

keyboardDrummer commented Jan 11, 2024 •

edited

Loading

keyboardDrummer Feb 9, 2024 •

edited

Loading

keyboardDrummer Feb 9, 2024 •

edited

Loading

keyboardDrummer Feb 9, 2024 •

edited

Loading

keyboardDrummer Feb 9, 2024 •

edited

Loading

keyboardDrummer Feb 9, 2024 •

edited

Loading

robin-aws Feb 12, 2024 •

edited

Loading