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

Try building with .NET 8.0 #5322

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Remove warnings with .NET 8.0
  • Loading branch information
atomb committed Apr 15, 2024
commit 8032f1d104f4db374fff388dc4910e01b5142e8b
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/SystemModuleManager.cs
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ public class SystemModuleManager {
Concat(TotalArrowTypeDecls.Keys.OrderBy(x => x)).
Concat(tupleInts.OrderBy(x => x));
var bytes = ints.SelectMany(BitConverter.GetBytes).ToArray();
hash = HashAlgorithm.Create("SHA256")!.ComputeHash(bytes);
hash = SHA256.Create()!.ComputeHash(bytes);
}

return hash;
Expand Down
4 changes: 3 additions & 1 deletion Source/DafnyCore/DafnyCore.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,9 @@
<TargetFramework>net8.0</TargetFramework>
<PackageLicenseExpression>MIT</PackageLicenseExpression>

<NoWarn>$(NoWarn);NU5104</NoWarn> <!-- Required because System.CommandLine is in beta. -->
<NoWarn>$(NoWarn);NU5104;CS8981</NoWarn>
<!-- NU5104 required because System.CommandLine is in beta. -->
<!-- CS8981 required because Dafny code can use lowercase type names -->
<IsPackable>true</IsPackable>
</PropertyGroup>

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ public class LargeFilesTest : ClientBasedLanguageServerTest {
var afterChange = DateTime.Now;
var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds;
await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout);
cancelSource.Cancel();
await cancelSource.CancelAsync();
var averageTimeToSchedule = await measurementTask;
var division = changeMilliseconds / openMilliseconds;
lowest = Math.Min(lowest, division);
Expand Down Expand Up @@ -114,4 +114,4 @@ public class LargeFilesTest : ClientBasedLanguageServerTest {

public LargeFilesTest(ITestOutputHelper output) : base(output) {
}
}
}
4 changes: 2 additions & 2 deletions Source/DafnyLanguageServer/Language/CachingParser.cs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ public class CachingParser : ProgramParser {
// Add NUL delimiter to avoid collisions (otherwise hash("A" + "BC") == hash("AB" + "C"))
var uriBytes = Encoding.UTF8.GetBytes(uri + "\0");

var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, HashAlgorithm.Create("SHA256")!);
var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, SHA256.Create()!);
if (!parseCache.TryGet(hash, out var result)) {
logger.LogDebug($"Parse cache miss for {uri}");
result = base.ParseFile(options, () => newReader, uri, cancellationToken);
Expand Down Expand Up @@ -83,4 +83,4 @@ public class CachingParser : ProgramParser {
result.Add(chunk);
}
}
}
}
4 changes: 2 additions & 2 deletions Source/DafnyLanguageServer/Language/CachingResolver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ public class CachingResolver : ProgramResolver {
private byte[] GetHash(ModuleDecl moduleDeclaration) {
if (!hashes.TryGetValue(moduleDeclaration, out var result)) {
var moduleVertex = dependencies.FindVertex(moduleDeclaration);
var hashAlgorithm = HashAlgorithm.Create("SHA256")!;
var hashAlgorithm = SHA256.Create()!;
hashAlgorithm.Initialize();
// We don't want the order of Successors to influence the hash, so we order by the content hash, for which CloneId is currently a proxy
var orderedSuccessors = moduleVertex.Successors.OrderBy(s => s.N.CloneId);
Expand All @@ -98,4 +98,4 @@ public class CachingResolver : ProgramResolver {

return result;
}
}
}
12 changes: 3 additions & 9 deletions Source/DafnyServer/SuperLegacySymbolTable.cs
Original file line number Diff line number Diff line change
Expand Up @@ -227,9 +227,7 @@ public class SuperLegacySymbolTable {
var updateStmt = (UpdateStmt)statement;
var leftSide = updateStmt.Lhss;
var rightSide = updateStmt.Rhss;
var leftSideDots = leftSide.OfType<ExprDotName>();
var rightSideDots = rightSide.OfType<ExprDotName>();
var allExprDotNames = leftSideDots.Concat(rightSideDots);
var allExprDotNames = leftSide.OfType<ExprDotName>();
foreach (var exprDotName in allExprDotNames) {
if (!(exprDotName.Lhs.Type is UserDefinedType)) {
continue;
Expand Down Expand Up @@ -304,12 +302,8 @@ public class SuperLegacySymbolTable {
var updateStmt = (UpdateStmt)statement;
var leftSide = updateStmt.Lhss;
var rightSide = updateStmt.Rhss;
var leftSideDots = leftSide.OfType<ExprDotName>();
var rightSideDots = rightSide.OfType<ExprDotName>();
var exprDotNames = leftSideDots.Concat(rightSideDots);
var leftSideNameSegments = leftSide.OfType<NameSegment>();
var rightSideNameSegments = rightSide.OfType<NameSegment>();
var nameSegments = leftSideNameSegments.Concat(rightSideNameSegments);
var exprDotNames = leftSide.OfType<ExprDotName>();
var nameSegments = leftSide.OfType<NameSegment>();
var allRightSideExpressions = rightSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions));
var allLeftSideExpressions =
leftSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions));
Expand Down