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

Fix 5746 #2

Draft
wants to merge 31 commits into
base: master
Choose a base branch
from
Draft

Fix 5746 #2

wants to merge 31 commits into from

Conversation

olivier-aws
Copy link
Owner

What was changed?

How has this been tested?

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

olivier-aws and others added 24 commits January 6, 2025 22:39
### Description
- Use .NET 8.0 instead of 6.0 throughout the project
- Make the ordering of diagnostics deterministic even when multiple
diagnostics differ only in their related locations

### How has this been tested?
- Updated existing tests to match well-defined ordering

<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 <[email protected]>
Fixes dafny-lang/ide-vscode#514

### What was changed?
Set a default verification time limit

### How has this been tested?
Added a CLI test that checks there is a default time-out

<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>
### What was changed?
- Remove the
`<RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>` property
from csproj files that was needed as a workaround but may break things
in .NET 8 according to SO
- Remove references from DafnyDriver to DafnyServer, that prevented
publishing correctly with .NET 8
- Stop publishing DafnyLanguageServer since it's not used directly.

### How has this been tested?
Tested by existing tests

<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 and others added 2 commits January 10, 2025 20:14
### 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
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants