Publish DafnyServer/Driver/Core to NuGet as well (#2787)

Fixes #2776: the root cause is that `DafnyLanguageServer` depends on `DafnyServer`, but the latter was never published. Also publishes the new `DafnyDriver` and `DafnyCore` packages I extracted out earlier, as otherwise the same problem would affect more packages on the next release. Also replaces `version.cs` with the more automatic mechanism of a `Build.Directory.props` file, just as Boogie uses. The side effect is that the version is more consistently aligned across all the published packages. In particular it changes the current `DafnyRuntime` version from `1.2.0` to `3.8.1.40901` (or rather `3.9.0` by the time we release this). I managed to augment the existing GHA that verifies the `dafny` dotnet tool to also do a very superficial verification that each library we publish can at least resolve all of its dependencies through NuGet.
dafny-lang · Sep 23, 2022 · b5b9019 · b5b9019
1 parent 2bc0042
commit b5b9019
Show file tree

Hide file tree

Showing 17 changed files with 79 additions and 90 deletions.
diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml
@@ -1,7 +1,17 @@
-name: Test NuGet Tool Installation
+name: Test NuGet Packages
 
 on:
   release:
+    # This triggers in response to a GitHub release being published,
+    # which happens to work well because we do that well after first publishing
+    # to NuGet. That gives at least 10 or 15 minutes for the newly published versions
+    # of these packages to be available for download here.
+    #
+    # Unfortunately that also means this doesn't trigger on the nightly build release,
+    # since that ends up updating an existing "nightly-..." release rather than creating a new one.
+    # For now that's a good thing since these jobs only test the latest actual released version,
+    # but ideally we'd fix both of those issues so that we test the fully NuGet publishing
+    # workflow in the nightly build.
     types: [ published ]
   # For manual testing through the Actions UI
   workflow_dispatch:
@@ -11,7 +21,7 @@ env:
   z3BaseUri: https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5
 
 jobs:
-  build:
+  test-dafny-cli-tool:
 
     runs-on: ${{ matrix.os }}
     strategy:
@@ -118,3 +128,36 @@ jobs:
     - name: Check Java compile
       run: |
         dafny /compile:3 /spillTargetCode:3 /compileTarget:java a.dfy
+
+  test-dafny-libraries:
+
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        # Hopefully we can automatically populate this list in the future,
+        # but note we need to skip Dafny since nuget install doesn't work for dotnet tools.
+        library-name: [ DafnyPipeline, DafnyServer, DafnyLanguageServer, DafnyRuntime, DafnyCore, DafnyDriver ]
+        # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
+        os: [ ubuntu-latest, ubuntu-18.04, macos-latest, windows-2019 ]
+        include:
+        - os:  'ubuntu-latest'
+          osn: 'ubuntu\-16.04'
+          z3: z3-4.8.5-x64-ubuntu-16.04
+        - os:  'ubuntu-18.04'
+          osn: 'ubuntu\-16.04'
+          z3: z3-4.8.5-x64-ubuntu-16.04
+        - os:  'macos-latest'
+          osn: 'osx-.*'
+          z3: z3-4.8.5-x64-osx-10.14.2
+        - os:  'windows-2019'
+          osn: 'win'
+          z3: z3-4.8.5-x64-win
+
+    steps:
+    ## Verify that the dependencies of the libraries we publish (e.g. DafnyLanguageServer)
+    ## are also published through NuGet.
+    ## Ideally we would have a test project that actually uses part of the public API of each package.
+    - name: Check library dependencies
+      run: |
+        nuget install ${{ matrix.library-name }}
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -8,8 +8,10 @@
 - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)
 - fix: Retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
 - fix: Correctly substitute variables introduced by a binding guard (https://github.com/dafny-lang/dafny/pull/2745)
+- fix: The CLI no longer attempts to load each DLL file passed to it. (https://github.com/dafny-lang/dafny/pull/2568)
 - fix: Improved hints and error messages regarding variance/cardinality preservation (https://github.com/dafny-lang/dafny/pull/2774)
 - feat: New behavior for `import opened M` where `M` contains a top-level declaration `M`, see PR for a full description (https://github.com/dafny-lang/dafny/pull/2355)
+- fix: The DafnyServer package is now published to NuGet as well, which fixes the previously-broken version of the DafnyLanguageServer package. (https://github.com/dafny-lang/dafny/pull/2787)
 
 # 3.8.1
 
@@ -46,7 +48,6 @@
 - fix: Improve the performance of proofs involving bit vector shifts (https://github.com/dafny-lang/dafny/pull/2520)
 - fix: Perform well-definedness checks for ensures clauses of forall statements (https://github.com/dafny-lang/dafny/pull/2606)
 - fix: Resolution and verification of StmtExpr now pay attention to if the StmtExpr is inside an 'old' (https://github.com/dafny-lang/dafny/pull/2607)
-- fix: The CLI no longer attempts to load each DLL file passed to it. (https://github.com/dafny-lang/dafny/pull/2568)
 
 # 3.7.3
 

diff --git a/Scripts/package.py b/Scripts/package.py
@@ -253,27 +253,27 @@ def pack(args, releases):
         run(["make", "--quiet", "refman"])
 
 def check_version_cs(args):
-    # Checking version.cs
-    with open(path.join(SOURCE_DIRECTORY,"version.cs")) as fp:
-        match = re.search(r'\[assembly:\s+AssemblyVersion\("([0-9]+.[0-9]+.[0-9]+).([0-9]+)"\)\]', fp.read())
+    # Checking Directory.Build.props
+    with open(path.join(SOURCE_DIRECTORY, "Directory.Build.props")) as fp:
+        match = re.search(r'\<VersionPrefix\>([0-9]+.[0-9]+.[0-9]+).([0-9]+)"\)', fp.read())
         if match:
             (v1, v2) = match.groups()
         else:
-            flush("The AssemblyVersion attribute in version.cs could not be found.")
+            flush("The AssemblyVersion attribute in Directory.Build.props could not be found.")
             return False
     now = time.localtime()
     year = now[0]
     month = now[1]
     day = now[2]
     v3 = str(year-2018) + str(month).zfill(2) + str(day).zfill(2)
     if v2 != v3:
-        flush("The date in version.cs does not agree with today's date: " + v3 + " vs. " + v2)
+        flush("The date in Directory.Build.props does not agree with today's date: " + v3 + " vs. " + v2)
     if "-" in args.version:
         hy = args.version[:args.version.index('-')]
     else:
         hy = args.version
     if hy != v1:
-        flush("The version number in version.cs does not agree with the given version: " + hy + " vs. " + v1)
+        flush("The version number in Directory.Build.props does not agree with the given version: " + hy + " vs. " + v1)
     if (v2 != v3 or hy != v1):
         return False
     flush("Creating release files for release \"" + args.version + "\" and internal version information: " + v1 + "." + v2)
@@ -284,7 +284,7 @@ def parse_arguments():
     parser.add_argument("version", help="Version number for this release")
     parser.add_argument("--os", help="operating system name for which to make a release")
     parser.add_argument("--skip_manual", help="do not create the reference manual")
-    parser.add_argument("--trial", help="ignore version.cs discrepancies")
+    parser.add_argument("--trial", help="ignore Directory.Build.props version discrepancies")
     parser.add_argument("--github_secret", help="access token for making an authenticated GitHub call, to prevent being rate limited.")
     parser.add_argument("--out", help="output zip file")
     return parser.parse_args()

diff --git a/Source/AutoExtern/AutoExtern.csproj b/Source/AutoExtern/AutoExtern.csproj
@@ -7,6 +7,7 @@
     <Nullable>enable</Nullable>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <GenerateTargetFrameworkAttribute>false</GenerateTargetFrameworkAttribute>
+    <IsPackable>false</IsPackable>
   </PropertyGroup>
 
   <ItemGroup>

diff --git a/Source/Dafny.sln b/Source/Dafny.sln
@@ -18,11 +18,6 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyDriver", "DafnyDriver\
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyServer", "DafnyServer\DafnyServer.csproj", "{71208DB9-31D6-4071-838B-8D44A37CF0F1}"
 EndProject
-Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{9542E008-355F-4A62-B262-A8DA314DA8C1}"
-	ProjectSection(SolutionItems) = preProject
-		version.cs = version.cs
-	EndProjectSection
-EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "IntegrationTests", "IntegrationTests\IntegrationTests.csproj", "{A4BC2C77-3A48-4917-AA22-41978DFFE24E}"
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "DafnyLanguageServer", "DafnyLanguageServer\DafnyLanguageServer.csproj", "{CD05D26C-C672-4F43-835E-7A3E1741E4D8}"

diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj
@@ -3,12 +3,11 @@
   <PropertyGroup>
       <OutputType>Exe</OutputType>
       <AssemblyName>Dafny</AssemblyName>
-      <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+      <GenerateAssemblyInfo>true</GenerateAssemblyInfo>
       <DefineConstants>TRACE</DefineConstants>
       <TargetFramework>net6.0</TargetFramework>
       <OutputPath>..\..\Binaries\</OutputPath>
       <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
-      <VersionPrefix>3.8.1.40901</VersionPrefix>
 
       <PackAsTool>true</PackAsTool>
       <ToolCommandName>dafny</ToolCommandName>
@@ -29,8 +28,4 @@
     <ProjectReference Include="..\DafnyDriver\DafnyDriver.csproj" />
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
-
-  <ItemGroup>
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
 </Project>
diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
@@ -19,7 +19,7 @@
     <DefineConstants>TRACE</DefineConstants>
     <TargetFramework>net6.0</TargetFramework>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
-    <IsPackable>false</IsPackable>
+    <IsPackable>true</IsPackable>
   </PropertyGroup>
 
   <ItemGroup>

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
@@ -11,7 +11,7 @@
 
       <PackageLicenseExpression>MIT</PackageLicenseExpression>
 
-      <IsPackable>false</IsPackable>
+      <IsPackable>true</IsPackable>
   </PropertyGroup>
 
   <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net6.0|AnyCPU'">
@@ -45,8 +45,4 @@
     <ProjectReference Include="..\DafnyTestGeneration\DafnyTestGeneration.csproj" />
     <ProjectReference Include="..\DafnyServer\DafnyServer.csproj" />
   </ItemGroup>
-
-  <ItemGroup>
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
 </Project>
diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj
@@ -8,7 +8,6 @@
     <RootNamespace>Microsoft.Dafny.LanguageServer</RootNamespace>
     <OutputPath>..\..\Binaries\</OutputPath>
     <IsPackable>true</IsPackable>
-    <VersionPrefix>3.8.1.40901</VersionPrefix>
     <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
   </PropertyGroup>
 
@@ -42,10 +41,6 @@
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
 
-  <ItemGroup>
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
-
   <ItemGroup>
     <Content Include="DafnyLanguageServer.appsettings.json">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>

diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj
@@ -7,7 +7,6 @@
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
     <OutputPath>..\..\Binaries\</OutputPath>
     <DefineConstants>TRACE</DefineConstants>
-    <VersionPrefix>3.8.0.40729</VersionPrefix>
     <TargetFramework>net6.0</TargetFramework>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
   </PropertyGroup>
@@ -57,8 +56,4 @@
     </EmbeddedResource>
   </ItemGroup>
 
-  <ItemGroup>
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
-
 </Project>
diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj
@@ -6,7 +6,6 @@
       <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
       <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
       <DefineConstants>TRACE;ISDAFNYRUNTIMELIB</DefineConstants>
-      <VersionPrefix>1.2.0</VersionPrefix>
       <TargetFramework>net6.0</TargetFramework>
       <OutputPath>..\..\Binaries\</OutputPath>
       <LangVersion>7.3</LangVersion>

diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj
@@ -5,8 +5,8 @@
       <AssemblyName>DafnyServer</AssemblyName>
       <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
       <DefineConstants>TRACE</DefineConstants>
-      <PackageVersion>1.1.0</PackageVersion>
       <TargetFramework>net6.0</TargetFramework>
+      <OutputPath>..\..\Binaries\</OutputPath>
   </PropertyGroup>
 
   <PropertyGroup Condition="'$(Configuration)|$(TargetFramework)|$(Platform)'=='Debug|net6.0|AnyCPU'">
@@ -22,8 +22,4 @@
   <ItemGroup>
     <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
   </ItemGroup>
-
-  <ItemGroup>
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
 </Project>
diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj
@@ -6,7 +6,6 @@
         <IsPackable>false</IsPackable>
         <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
         <DefineConstants>TRACE</DefineConstants>
-        <PackageVersion>1.1.0</PackageVersion>
         <TargetFramework>net6.0</TargetFramework>
         <Nullable>enable</Nullable>
         <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
@@ -17,8 +16,4 @@
       <ProjectReference Include="..\DafnyPipeline\DafnyPipeline.csproj" />
     </ItemGroup>
 
-    <ItemGroup>
-        <Compile Include="..\version.cs" />
-    </ItemGroup>
-
 </Project>
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -1,8 +1,11 @@
 <Project>
 
-  <!-- Target framework -->
   <PropertyGroup>
+    <!-- Target framework -->
     <TargetFramework>net6.0</TargetFramework>
+
+    <!-- Version 3.8.1, year 2018+4, month 9, day 1 -->
+    <VersionPrefix>3.8.1.40901</VersionPrefix>
   </PropertyGroup>
 
 </Project>
diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj
@@ -5,6 +5,7 @@
         <TargetFramework>net6.0</TargetFramework>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
+        <IsPackable>false</IsPackable>
     </PropertyGroup>
 
     <ItemGroup>

diff --git a/Source/version.cs b/Source/version.cs
diff --git a/docs/dev/RELEASE.md b/docs/dev/RELEASE.md
@@ -19,16 +19,8 @@
    use judgement. The last section is in "ymmdd" format, where "y" is
    the number of years since 2018 and "mmdd" the month and day portions
    of the release date (e.g., a release on January 12th, 2022 would be
-   x.y.z.40112). Edit the internal version number in the following
-   places:
-
-   * `Source/version.cs`
-
-   * `Source/Dafny/Dafny.csproj`
-
-   * `Source/DafnyPipeline/DafnyPipeline.csproj`
-
-   * `Source/DafnyLanguageServer/DafnyLanguageServer.csproj`
+   x.y.z.40112). Edit the internal version number in 
+  `Source/Directory.Build.Props`.
 
    Put the public version number in place of the "Upcoming" header in
    `RELEASE_NOTES.md`, and add a new "Upcoming" header above it.
@@ -54,8 +46,9 @@
    ```
 
 5. A GitHub action will automatically run in reaction to the tag being pushed,
-   which will build the artifacts and reference manual and then create a draft
-   GitHub release. You can find and watch the progress of this workflow at
+   which will build the artifacts, upload them to NuGet, build the reference manual,
+   and then create a draft GitHub release.
+   You can find and watch the progress of this workflow at
    https://github.com/dafny-lang/dafny/actions.
 
 6. Once the action completes, you should find the draft release at
@@ -65,35 +58,24 @@
    the release, if this is not a pre-release.
 
 7. Push the "Publish" button. This will trigger yet another workflow
-   that will download the published artifacts and run a smoke test
-   on multiple platforms. Again you can watch for this workflow at
+   that will download the published artifacts (from both GitHub and NuGet)
+   and run a smoke test on multiple platforms. 
+   Again you can watch for this workflow at
    https://github.com/dafny-lang/dafny/actions.
 
-8. Manually upload packages to NuGet, from the fresh checkout of the
-   repository used for tagging.
-
-   ```
-   dotnet build Source/Dafny.sln
-   dotnet pack --no-build dafny/Source/Dafny.sln
-   dotnet nuget push --skip-duplicate "Binaries/Dafny*.nupkg" -k $A_VALID_API_KEY -s https://api.nuget.org/v3/index.json
-   ```
-
-9. Manually trigger the "Test NuGet Tool Installation" workflow on the
-   `master` branch (following the same process as for step 3).
-
-10. If preparing a pre-release, stop here, as
-    the following steps declare the release as the latest version, which
-    is not the intention.
+8. If preparing a pre-release, stop here, as
+   the following steps declare the release as the latest version, which
+   is not the intention.
 
-11. If something goes wrong, delete the tag and release in GitHub, fix the
-    problem and try again.
+9. If something goes wrong, delete the tag and release in GitHub, fix the
+   problem and try again.
 
-12. Update the Homebrew formula for Dafny (see below).
+10. Update the Homebrew formula for Dafny (see below).
     Note that it is fine to leave this for the next day,
     and other members of the community may update the formula
     in the meantime anyway.
 
-13. Announce the new release to the world.
+11. Announce the new release to the world.
 
 ## Updating Dafny on Homebrew