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>
dafny-lang · Jan 10, 2025 · 0edf705 · 0edf705
1 parent c79cb5e
commit 0edf705
Show file tree

Hide file tree

Showing 8 changed files with 6 additions and 27 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -15,7 +15,6 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>