Update to .NET 8 #5322

atomb · 2024-04-15T16:43:57Z

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

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

tchajed · 2024-09-16T20:53:02Z

I think it would be good to revisit this. Homebrew has deprecated the Dafny formula because it depends on dotnet 6 which is no longer supported upstream.

keyboardDrummer · 2024-09-17T09:12:35Z

I think it would be good to revisit this. Homebrew has deprecated the Dafny formula because it depends on dotnet 6 which is no longer supported upstream.

Agreed. Would be good for Dafny development itself as well.

keyboardDrummer · 2024-11-06T09:59:41Z

Fuel.legacy.dfy test becomes non-deterministic with this change. It flips between:

 Fuel.legacy.dfy(335,26): Error: function precondition could not be proved
 Fuel.legacy.dfy(324,21): Related location
-Fuel.legacy.dfy(313,41): Related location
+Fuel.legacy.dfy(314,46): Related location

Both error messages are valid, since they point to two different failing cases of a match.

.bpl files between conflicting runs are the same

Using /vcsCores:1 does not resolve the issue

…ve duplicates

keyboardDrummer · 2025-01-07T13:29:20Z

Non-determinism issue has been resolved.

robin-aws · 2025-01-07T16:13:53Z

.github/workflows/doc-tests.yml

@@ -37,7 +37,7 @@ jobs:
    - name: Setup dotnet
      uses: actions/setup-dotnet@v4
      with:
-        dotnet-version: 6.0.x
+        dotnet-version: 8.0.x


Okay now we really are installing the same version of .NET twice in several workflows, and my comments from an earlier PR to remove the duplication actually apply now :)

robin-aws · 2025-01-07T16:22:54Z

Source/AutoExtern.Test/AutoExtern.Test.csproj

@@ -2,7 +2,7 @@

  <PropertyGroup>
    <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>


Could this be moved to Directory.Build.props so it only appears once?

robin-aws · 2025-01-07T16:25:24Z

Source/DafnyServer/SuperLegacySymbolTable.cs

-      var leftSideDots = leftSide.OfType<ExprDotName>();
-      var rightSideDots = rightSide.OfType<ExprDotName>();
-      var allExprDotNames = leftSideDots.Concat(rightSideDots);
+      var allExprDotNames = leftSide.OfType<ExprDotName>();


Why did this change?

@atomb made this change. Rider confirms it's a noop:

Same for the other one I imagine.

Ah got it, definitely not obvious without context

robin-aws · 2025-01-07T16:27:13Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect

How did Fuel.legacy.dfy.expect ever work before?

I think it relied on the undefined but deterministic ordering of something, like enumerating over a dictionary. I'm guessing there was a performance improvement in .NET that made this undefined ordering also non-deterministic, which caused the test to become unstable until I added an explicit ordering.

robin-aws · 2025-01-07T16:30:31Z

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -67,7 +67,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
      wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
      wr.WriteLine("// To recompile, you will need the libraries");
      wr.WriteLine("//     System.Runtime.Numerics.dll System.Collections.Immutable.dll");
-      wr.WriteLine("// but the 'dotnet' tool in net6.0 should pick those up automatically.");
+      wr.WriteLine("// but the 'dotnet' tool in net8.0 should pick those up automatically.");


Suggested change

wr.WriteLine("// but the 'dotnet' tool in net8.0 should pick those up automatically.");

wr.WriteLine("// but the 'dotnet' tool in .NET should pick those up automatically.");

Just to avoid some diffs the next time we upgrade.

robin-aws

Excelsior!

### 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]>

atomb added 10 commits April 15, 2024 09:43

Try building with .NET 8.0

13593d4

Update CI to install .NET 8.0

80eef37

Use .NET 8.0 when executing generated C# code

929e8d5

Update installation docs to use .NET 8.0

9a4b7c2

Make pre-commit hook match CI checks

d468f1d

Update formatting of DafnyRuntimeSystemModule

c584c06

Remove warnings with .NET 8.0

8032f1d

Fix message coming from .NET standard libraries

e19bc59

Fix fragile test output

b0d5543

Disable lowercase class name warnings

b2bae1e

atomb self-assigned this Apr 15, 2024

atomb mentioned this pull request Apr 23, 2024

Support dotnet 8 #4948

Open

chenrui333 mentioned this pull request Oct 6, 2024

dafny: align deprecation with dotnet@6 and drop Ventura bottle Homebrew/homebrew-core#182283

Merged

6 tasks

keyboardDrummer added 4 commits November 4, 2024 17:13

Merge remote-tracking branch 'origin/master' into net8.0

66d1327

Update Tomlyn

4981f2a

Update fuel test

19ae7d7

Update patch file

5b21870

keyboardDrummer added 7 commits December 19, 2024 17:13

Merge remote-tracking branch 'origin/master' into net8.0

b991205

Switch Fuel.legacy to the new CLI, and update its expect file to remo…

74d5512

…ve duplicates

Merge remote-tracking branch 'origin/master' into net8.0

403d224

Update test to use new CLI

053a32e

Updates

f08c197

Refactoring

1a70cae

Merge branch 'net8.0' of github.com:keyboardDrummer/dafny into net8.0

2dd37d1

keyboardDrummer marked this pull request as ready for review January 7, 2025 13:28

keyboardDrummer changed the title ~~Try building with .NET 8.0~~ Update to .NET 8 Jan 7, 2025

keyboardDrummer enabled auto-merge (squash) January 7, 2025 13:29

keyboardDrummer added 2 commits January 7, 2025 14:33

Ran formatter

4628124

Update expect files

209530f

robin-aws requested changes Jan 7, 2025

View reviewed changes

keyboardDrummer added 5 commits January 7, 2025 17:41

Simplify CI files, update doc-test expect file

7651291

Update expect files

33a8670

Use Directory.Build.props

4925fe2

Fix

a13764f

Update DafnyRuntimeSystemModule.cs

b9a2c9b

keyboardDrummer requested a review from robin-aws January 8, 2025 10:02

keyboardDrummer disabled auto-merge January 8, 2025 10:03

keyboardDrummer enabled auto-merge (squash) January 8, 2025 10:03

robin-aws approved these changes Jan 8, 2025

View reviewed changes

keyboardDrummer merged commit 0831717 into dafny-lang:master Jan 8, 2025
22 checks passed

alexstaeding mentioned this pull request Feb 10, 2025

dafny: 4.9.1 -> 4.10.0 NixOS/nixpkgs#380907

Merged

13 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update to .NET 8 #5322

Update to .NET 8 #5322

atomb commented Apr 15, 2024 •

edited by keyboardDrummer

Loading

tchajed commented Sep 16, 2024

keyboardDrummer commented Sep 17, 2024

keyboardDrummer commented Nov 6, 2024 •

edited

Loading

keyboardDrummer commented Jan 7, 2025

robin-aws Jan 7, 2025

robin-aws Jan 7, 2025

robin-aws Jan 7, 2025

keyboardDrummer Jan 7, 2025

robin-aws Jan 7, 2025

robin-aws Jan 7, 2025

keyboardDrummer Jan 7, 2025 •

edited

Loading

robin-aws Jan 7, 2025

robin-aws left a comment

	wr.WriteLine("// but the 'dotnet' tool in net8.0 should pick those up automatically.");
	wr.WriteLine("// but the 'dotnet' tool in .NET should pick those up automatically.");

Update to .NET 8 #5322

Update to .NET 8 #5322

Conversation

atomb commented Apr 15, 2024 • edited by keyboardDrummer Loading

Description

How has this been tested?

tchajed commented Sep 16, 2024

keyboardDrummer commented Sep 17, 2024

keyboardDrummer commented Nov 6, 2024 • edited Loading

keyboardDrummer commented Jan 7, 2025

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

keyboardDrummer Jan 7, 2025

Choose a reason for hiding this comment

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

keyboardDrummer Jan 7, 2025 • edited Loading

Choose a reason for hiding this comment

robin-aws Jan 7, 2025

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

atomb commented Apr 15, 2024 •

edited by keyboardDrummer

Loading

keyboardDrummer commented Nov 6, 2024 •

edited

Loading

keyboardDrummer Jan 7, 2025 •

edited

Loading