Deduplicate verification diagnostic reporting between CLI and server #5246
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…g#5317) ### Description Adds a first pass of proof obligation description expressions, towards resolving dafny-lang#2987. It also adds a new hidden option, `--show-proof-obligation-expressions`, which adds to each (supported) failed proof obligation error message an equivalent Dafny assertion. This option is used to automate tests for the newly added proof obligation description expressions, but this PR does not backfill tests for existing PODesc expressions. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
This PR changes the remaining 5 of the 10 `dafny0/ResolutionErrors*.dfy` tests so that they test not only the legacy resolver, but also the resolver refresh. * fix: Remove `this` from the scope when resolving `static const` fields * fix: Remove `this` from the scope when resolving type constraints and type witnesses * Adjust tests and expected output for `dafny0/ResolutionErrors[45679].dfy` * Add test for for unary TLA-style expressions (these worked, but did not have specific tests) * chore: Remove `TernaryExpr.PrefixEqUsesNat`, which wasn't needed ### Regression The one place where the new type inference was not able to do as well as the old is the code snippet ``` dafny var c := d; var xx := c[25..50][10].x; ``` from `dafny0/ResolutionErrors4.dfy`. Here, the new resolver does not thread the element type of `d` through the array-to-sequence conversion `c[25..50]`, and therefore the `.x` gives an error. The workaround is to declare the type of `c` explicitly in the code. I don't see a quick fix for this in the type inference. A good improvement, which I believe would also fix this problem, is to do member resolution (like `.x`) lazily instead of eagerly. This would allow the type-inference machinery to start making some decisions, which will lead to it figuring out a type for `c`, after which types for the other expressions, including the `.x`, can be inferred. I would love to see this improvement in the type inference, and the new resolver has "guarded constraints" that exist in order to lazy inference. However, such a change will take some effort, because the methods that currently try to do member lookup too easily generate errors (rather than saying "please try again later"). Such a change is out of scope for this PR. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description The previous implementation had two issues: * It displayed only the milliseconds portion of the duration, so would be incorrect for any verification lasting longer than a second. * The use of exponential notation for resource count made it more difficult to compare values, and impossible to identify small differences. This also changes the overall format of the message slightly. ### How has this been tested? Existing tests have been updated to reflect the changes in formatting. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Build against the newer GoLang 1.22, since the download for 1.15 seems to have been taken down <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…g#5329) ### Description - Refactoring: let `Method` and `Function` share the field `Ins` (for inputs) and the related property `HasPreconditions`, using the class `MethodOrFunction`. - Do not refer to auditor code when building a Dafny library - Previously, using `{:termination false}` in a library was not allowed, but after this PR it is. I believe it should be allowed, since currently there is no workaround. - For all "auditor assumptions" that had `allowedInLibraries: false`, there were existing warnings for: - assume without `{:axiom}` - forall without a body - loop without a body - functions or methods without a body - usage of `{:only}` - For the other "auditor assumptions", new warnings have been added. - Emit a warning when `{:verify false}` is used - Emit a warning when exporting a declaration that has requires clauses or subset type inputs - Emit a warning when importing a declaration that has ensures clauses or subset type outputs - Add an option `--allow-external-contracts` that silences the previous two warnings. - Add warning for bodyless functions marked with {:extern}, and an option `--allow-external-function` to silence this warning. - I have decided not to warn on `{:assume_concurrent}` without `{:axiom}`, since the `{:assume_concurrent}` attribute is only useful when using `{:concurrent}`, which you would add in a rather late stage anyways. ### How has this been tested? - Updated CLI tests for the new warnings and options <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description Turning on doofiles/Test4.dfy ### How has this been tested? It's adding a test <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description This PR implements most immutable types in Dafny (Sequence, Set, Multiset, Map) and implements most if not all operators on them. It also sets an architecture that can now be relied on. List of features in this PR: - More comprehensive Rust AST, precedence and associativity to render parentheses - The Rust compiler no longer crash when not in /runAllTests, but emits invalid code. It makes it possible to see which features are missing by searching for `<i>` in the generated code. - Made verification of GenExpr less brittle - Previous PR review comments - Ability to use shadowed identifiers to avoid numbers in names. Rust has the same rules as Dafny for shadowing, and I will continue to monitor cases where semantics might differ. ### How has this been tested? I added an integration test for compiling Dafny to Rust, and I added unit tests for the runtime in Rust *All tests for each compiler now have a `.rs.check` if they fail.*. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
…)" (dafny-lang#5377) This reverts commit 3e38580 to fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/8868313153 --------- Co-authored-by: Fabio Madge <fmadge@amazon.com>
### Changes - To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to `--library`. This does the following: 1. Call `dafny build -t:lib` using the project file to get a doo file. In the future we plan to let this be a NOOP if the right build file is already there. 1. Replace the usage of the project file in the origin call to `dafny`, with this doo file. - Extract code from `DafnyFile.CreateAndValidate` into methods - When parsing a file, correctly pass parse options to included files. This does not have any particular affect because only doo files are passed with different options, and those do not use includes. However, doing this does seem more correct and it was useful previously, so I'll keep it in. - Move `ReadsClausesOnMethods` option code - Do not let project files include themselves through something like `includes = ["**/*"]` ### How has this been tested? - Add the CLI test `projectAsLibrary.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
This PR is a replay of dafny-lang#5081 after fixing the issue with the paths too long for Windows, so it should no longer break the CI. ### Description This PR implements most immutable types in Dafny (Sequence, Set, Multiset, Map) and implements most if not all operators on them. It also sets an architecture that can now be relied on. List of features in this PR: - More comprehensive Rust AST, precedence and associativity to render parentheses - The Rust compiler no longer crash when not in /runAllTests, but emits invalid code. It makes it possible to see which features are missing by searching for `<i>` in the generated code. - Made verification of GenExpr less brittle - Previous PR review comments - Ability to use shadowed identifiers to avoid numbers in names. Rust has the same rules as Dafny for shadowing, and I will continue to monitor cases where semantics might differ. ### How has this been tested? I added an integration test for compiling Dafny to Rust, and I added unit tests for the runtime in Rust *All tests for each compiler now have a `.rs.check` if they fail.*. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
…ng#5361) This reverts commit 44ca1b2. ### Description The recently merged PR dafny-lang#5342 argues that we should automatically retry failing IDE tests, because that's what we manually do anyways. However, we only do that in some cases. Specifically, when any of us make changes that may create unstable tests, such as changes in the IDE, then failing IDE tests should not be retried, manually or automatically. PR5342 makes it so that such a retry happens automatically, thereby making it much easier to introduce non-deterministic bugs either in IDE code or tests. That's why this PR is reverting that one. IMO there is little difference between a test that fails 100% of the time and one that fails <100% of the time. Retrying a failing test that fails <100% of the time is similar to saying "I believe my PR is not at fault for this test failing, please ignore it". A similar situation occurs when a PR gets merged that causes nightly to fail. However then we don't have a way for new PRs to say "please ignore nightly failing", and we explicitly block all PR until nightly is fixed again. A similar approach to unstable tests would be to not to retry failing builds until the instability is resolved, but instead to wait until an instability fix PR is merged. ### How has this been tested? It's a revert. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description Remove 'note,' at the start of some warnings ### How has this been tested? Updated expect files <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
…-lang#5347) This PR fixes the standard library so that it is compatible with general newtypes. Fixes dafny-lang#5345 ### How has this been tested? I added a verification test for just a small project with a dfyconfig file including the standard library <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Fabio Madge <fmadge@amazon.com>
This reverts commit 0b629ea to fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/8896634004/job/24436389955 Unfortunately I approved dafny-lang#5380 before all of the deep tests had run, and because the extra checks aren't normally run for a PR unless it has the `run-deep-tests` label, they can't be required checks, so the PR was auto-merged even though several Windows runs timed out after 2 hours.
Fixes dafny-lang#5337 ### Description - Add the field `base` to Dafny project files, which allows a project file to inherit fields from another one. Options from the current file override options from the base. Includes from the current file override excludes from the base, and excludes from the current file override includes from the base. The base may itself also have a base. - Small improvements to project file error reporting. See the updates in existing tests for more information. ### How has this been tested? - Added the test `cli/projectFile/base/included.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description Merging from the released 4.6 branch. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Remy Willems <rwillems@amazon.com>
### Description Add more logging to QuickEditsInLargeFile ### How has this been tested? Test logging change, no additional tests needed <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description Setting up a daily scheduled build to run the LSP tests 5 times on each platform, in an effort to proactively uncover flaky test failures that show up at the worst possible time as you're trying to get your wonderful PR you've been working on for weeks merged or even worse that break the nightly build for the third day in a row forcing the team to drop everything to click Retry Failed Jobs two or three times before ANY PRs can be merged not that I'm frustrated or anything. :) The PR CI was previously running the LSP tests twice every time for the same reason. Given this daily job will soak them more deeply, and that the `osx` unit test job on PRs in particular has been taking almost 45 minutes and becoming the limiting factor, I've opted to just run them once on PRs now. Note that unlike the original double run, it was simpler to use matrices just as we do for integration tests, only in this case just iterating the same test run in parallel 5 times. It's possible running twice on the same runner might trigger more failures, but it seems unlikely since the second run happens in a fresh process and no state leaks between the runs AFAICT. ### How has this been tested? Dry-run on my fork: https://github.com/robin-aws/dafny/actions/runs/8914692810 I've run it a few times without any failures yet, but we'll have to see what happens after a week or so of scheduled runs. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description - Fix bug in reporting of time taken when a verification timeout occurs - Make test 3855 stable by redacting the time taken ### How has this been tested? - Fix is not tested - Flaky test is updated <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang#5386) ### Changes Fix a bug in AwaitNextNotificationAsync that prevented the 'Waited for' log line to show up, to help debug dafny-lang#5384 ### Testing Since this was a bug in the testing code, I'm OK with not testing it. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Fixes dafny-lang#4985 ### Description #### Main Change Options come in several flavors. Some options do not affect the correctness of the program, such as those that affect logging or performance. Other options do affects the semantics. These may be configurable per module, such as `function-syntax`, or they may be 'global', which means the value this has for a dependency affects what value it should have for the dependent, such as `unicode-char` or `allow-warnings`. Previously, options were only marked as global or not, so it was not possible to distinguish between non-semantic options and semantic options that are configurable at the module level. This PR adds registration to make that distinction, and uses that to determine which module level options to track in doo files, which fixes bugs that would occur when using non-default values for these options in combination with doo files. #### Minor changes - Fix a bug that would prevent using Doo files, due to their read stream being disposed before they were fully read. - Add a hidden option `--hidden-no-verify` that allows building doo files without verifying then, as if you had verified them. This is useful for building and committing the standard library without verifying it, which is safe because CI will still build it with verification as well. ### How has this been tested? - Added the test `semanticOptions.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
### Description <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix for an issue visible in the latest release? Mention this in the PR details and ensure a patch release is considered --> This PR adds support for passing `--go-module-name` flag to the translate go command to conform to the Go Module project structure. Example: CLI: `dafny translate go --go-module-name MyModule` It also uses `dtr` files to fetch the right `go-module-name` for dependencies. ### How has this been tested? <!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` --> Added integration tests which use checked-in DafnyRuntimeGo libs using the `replace` `go.mod` directive. See the `go-module` directory. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
### Description Introduce a new option `--unsafe-dependencies` which is always on for `dafny server` and `dafny resolve`, optionally enabled for `dafny verify`, and off for all other commands. This option only affects compilation when a dependency (--library) is specified using a Dafny project file. In case the option is off, that dependency project is used to build a library file, which is then used as the dependency. In case the option is on, the source files from the dependency project are included but not verified or translated. The goal of this PR is to to enable practical development of Dafny projects where multiple projects that depend on each other live inside a single repository, while not affecting the CI of Dafny projects in any way. ### How has this been tested? - Updated the test projectAsLibrary <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Mature the
IPhaseconcept by bigger use of it in more locations. In particular, it is now used for verification and verification coverage diagnostics.Specific changes:
Compilation(the back-end) report verification diagnostics, instead of the two front-endsIdeState.HandleBoogieUpdate(IDE) andVerifyCommand.ReportVerificationDiagnostics(CLI), reducing duplication.CompilationcallWarnAboutSuspiciousDependenciesForScopeinstead ofIdeState.HandleBoogieUpdate(IDE) andVerifyCommand.LogVerificationResults(CLI), reducing duplication.How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.