Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Delete test for legacy CLI that tests ambiguous behavior #6037

Merged

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Jan 10, 2025

Should fix failing nightly: https://github.com/dafny-lang/dafny/actions/runs/12711494070/job/35434956978

What was changed?

The Dafny legacy CLI shows part of a .NET error message as part of it UI. This can not be tested well since the specific error message is not defined as part of .NET, and can be different across .NET versions and platforms.

On Windows it returns:
Invalid filename: The value cannot be an empty string. (Parameter 'path')
On other platforms it is:
Invalid filename: The path is empty. (Parameter 'path')

Instead of fixing the legacy CLI to remove the ambiguity, I'm removing the test for that ambiguous behavior since the old CLI is deprecated.

How has this been tested?

Removed a test

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

@keyboardDrummer keyboardDrummer added the run-integration-tests Forces running the CI for integration tests even if the deep tests fail label Jan 10, 2025
@keyboardDrummer keyboardDrummer enabled auto-merge (squash) January 10, 2025 15:50
@keyboardDrummer keyboardDrummer changed the title Delete test for legacy CLI that tests broken behavior Delete test for legacy CLI that tests ambiguous behavior Jan 10, 2025
@olivier-aws olivier-aws added the run-deep-tests Tells CI to run all tests label Jan 10, 2025
@keyboardDrummer keyboardDrummer merged commit 8ede38c into dafny-lang:master Jan 10, 2025
26 of 31 checks passed
@keyboardDrummer keyboardDrummer deleted the deleteLegacyCliTest branch January 10, 2025 20:55
olivier-aws pushed a commit to olivier-aws/dafny that referenced this pull request Jan 13, 2025
### What was changed?
The Dafny legacy CLI shows part of a .NET error message as part of it
UI. This can not be tested well since the specific error message is not
defined as part of .NET, and can be different across .NET versions and
platforms.

On Windows it returns:
`Invalid filename: The value cannot be an empty string. (Parameter
'path')`
On other platforms it is:
`Invalid filename: The path is empty. (Parameter 'path')`

Instead of fixing the legacy CLI to remove the ambiguity, I'm removing
the test for that ambiguous behavior since the old CLI is deprecated.

### How has this been tested?
Removed 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
run-deep-tests Tells CI to run all tests run-integration-tests Forces running the CI for integration tests even if the deep tests fail
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants