diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index 2bf2fbb4a9b..1d0da68a811 100644 --- 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 index 38e7c6883dd..c680ca2095e 100644 --- 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 index 61420509aa5..b92eeb26092 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -253,13 +253,13 @@ 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'\([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] @@ -267,13 +267,13 @@ def check_version_cs(args): 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 index 5d608ec636e..97e0c970fde 100644 --- a/Source/AutoExtern/AutoExtern.csproj +++ b/Source/AutoExtern/AutoExtern.csproj @@ -7,6 +7,7 @@ enable false false + false diff --git a/Source/Dafny.sln b/Source/Dafny.sln index ddfd6d91f5f..990dfb06835 100644 --- 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 index 4fe649292b7..59c45499978 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -3,12 +3,11 @@ Exe Dafny - false + true TRACE net6.0 ..\..\Binaries\ false - 3.8.1.40901 true dafny @@ -29,8 +28,4 @@ - - - - diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index a9e188817c1..d4a5a16b17b 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -19,7 +19,7 @@ TRACE net6.0 MIT - false + true diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 87eb8283882..f7d1e667c6a 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -11,7 +11,7 @@ MIT - false + true @@ -45,8 +45,4 @@ - - - - diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 68d9d9580f7..adc6acf25a3 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -8,7 +8,6 @@ Microsoft.Dafny.LanguageServer ..\..\Binaries\ true - 3.8.1.40901 false @@ -42,10 +41,6 @@ - - - - PreserveNewest diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 14daf412475..e7d3f44d800 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -7,7 +7,6 @@ false ..\..\Binaries\ TRACE - 3.8.0.40729 net6.0 MIT @@ -57,8 +56,4 @@ - - - - diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 7ed862a4be6..a829585f779 100755 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -6,7 +6,6 @@ true false TRACE;ISDAFNYRUNTIMELIB - 1.2.0 net6.0 ..\..\Binaries\ 7.3 diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 654e2a5adb6..044ef43d1da 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,8 +5,8 @@ DafnyServer false TRACE - 1.1.0 net6.0 + ..\..\Binaries\ @@ -22,8 +22,4 @@ - - - - diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 72df387942f..b59b9ef8d48 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -6,7 +6,6 @@ false false TRACE - 1.1.0 net6.0 enable false @@ -17,8 +16,4 @@ - - - - diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index fc397c82c2e..73fe5ea932a 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,8 +1,11 @@ - + net6.0 + + + 3.8.1.40901 diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index ba95cfed35a..8dd1ca9d820 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -5,6 +5,7 @@ net6.0 enable enable + false diff --git a/Source/version.cs b/Source/version.cs deleted file mode 100644 index 36a5575ea00..00000000000 --- a/Source/version.cs +++ /dev/null @@ -1,8 +0,0 @@ -using System.Reflection; -// Version 3.7.3, year 2018+4, month 7, day 19 -// When changing this, also be sure to change it in the following files: -// * Source/Dafny/Dafny.csproj -// * Source/DafnyPipeline/DafnyPipeline.csproj -// * Source/DafnyLanguageServer/DafnyLanguageServer.csproj -[assembly: AssemblyVersion("3.8.1.40901")] -[assembly: AssemblyFileVersion("3.8.1.40901")] diff --git a/docs/dev/RELEASE.md b/docs/dev/RELEASE.md index 2012f873360..6e9cc2b2bad 100644 --- 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