From 0edf705ee7a5a53cc496d1718aa36351d10fb3d2 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Fri, 10 Jan 2025 15:20:59 +0100
Subject: [PATCH] Attempt at fixing nightly. (#6035)

### 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>
---
 .github/workflows/integration-tests-reusable.yml     |  5 +++++
 Scripts/package.py                                   |  1 -
 Source/DafnyDriver/Commands/ServerCommand.cs         |  2 --
 Source/DafnyDriver/DafnyDriver.csproj                | 12 +-----------
 .../Legacy/LegacyJsonVerificationLogger.cs           |  1 -
 .../DafnyLanguageServer/DafnyLanguageServer.csproj   |  1 -
 Source/DafnyServer/DafnyServer.csproj                | 10 ----------
 .../DafnyTestGeneration/DafnyTestGeneration.csproj   |  1 -
 8 files changed, 6 insertions(+), 27 deletions(-)

diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml
index 3109c167ccb..79d72f30dcf 100644
--- a/.github/workflows/integration-tests-reusable.yml
+++ b/.github/workflows/integration-tests-reusable.yml
@@ -72,6 +72,11 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
+    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
     - name: C++ for ubuntu 20.04
       if: matrix.os == 'ubuntu-20.04'
       run: |
diff --git a/Scripts/package.py b/Scripts/package.py
index f543d37715c..aaffbfe4e20 100755
--- a/Scripts/package.py
+++ b/Scripts/package.py
@@ -161,7 +161,6 @@ def build(self):
         if path.exists(self.buildDirectory):
             shutil.rmtree(self.buildDirectory)
         run(["make", "--quiet", "clean"])
-        self.run_publish("DafnyLanguageServer")
         self.run_publish("DafnyServer")
         self.run_publish("DafnyRuntime", "netstandard2.0")
         self.run_publish("DafnyRuntime", "net452")
diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs
index a4cdf8c92b3..51381672ef5 100644
--- a/Source/DafnyDriver/Commands/ServerCommand.cs
+++ b/Source/DafnyDriver/Commands/ServerCommand.cs
@@ -1,6 +1,4 @@
-using System.Collections.Generic;
 using System.CommandLine;
-using DafnyCore;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index f928e3f5043..0236f2ce5f6 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -13,16 +13,6 @@
 
       <IsPackable>true</IsPackable>
   </PropertyGroup>
-
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
     
   <ItemGroup>
     <PackageReference Include="Microsoft.TestPlatform.Extensions.TrxLogger" Version="17.9.0" />
@@ -42,8 +32,8 @@
     
   <ItemGroup>
     <ProjectReference Include="..\DafnyCore\DafnyCore.csproj" />
+    <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
   </ItemGroup>
   
   <ItemGroup>
diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
index 93087fe8e5d..e6e27c8b151 100644
--- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
+++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs
@@ -4,7 +4,6 @@
 using System.Linq;
 using System.Text.Json.Nodes;
 using DafnyCore.Verifier;
-using DafnyServer;
 using Microsoft.Boogie;
 using VC;
 
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
index 67513425d4e..92f1fad7dff 100644
--- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
+++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
@@ -6,7 +6,6 @@
     <Nullable>enable</Nullable>
     <RootNamespace>Microsoft.Dafny.LanguageServer</RootNamespace>
     <OutputPath>..\..\Binaries\</OutputPath>
-    <IsPackable>true</IsPackable>
     <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
     <PackageReadmeFile>README.md</PackageReadmeFile>
diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj
index d736ee1074e..f9cd46eb532 100644
--- a/Source/DafnyServer/DafnyServer.csproj
+++ b/Source/DafnyServer/DafnyServer.csproj
@@ -10,16 +10,6 @@
       <PackageLicenseExpression>MIT</PackageLicenseExpression>
   </PropertyGroup>
 
-  <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net8.0|AnyCPU'">
-    <AppendTargetFrameworkToOutputPath>false</AppendTargetFrameworkToOutputPath>
-    <AppendRuntimeIdentifierToOutputPath>false</AppendRuntimeIdentifierToOutputPath>
-  </PropertyGroup>
-
-  <!-- Working around some stange behavior in dotnet publish: https://github.com/dotnet/sdk/issues/10566 -->
-  <PropertyGroup Condition="$(RUNTIME_IDENTIFIER) != ''">
-    <RuntimeIdentifier>$(RUNTIME_IDENTIFIER)</RuntimeIdentifier>
-  </PropertyGroup>
-
   <ItemGroup>
     <ProjectReference Include="..\DafnyLanguageServer\DafnyLanguageServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
index 016cf01c491..f4f2f78ffd1 100644
--- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
+++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
@@ -15,7 +15,6 @@
   </PropertyGroup>
   
   <ItemGroup>
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>