Let DafnyRuntime target more frameworks
#2604
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
fabiomadge
reviewed
Aug 17, 2022
.github/workflows/msbuild.yml
Outdated
Comment on lines
50
to
51
| dotnet build -f net462 Source/DafnyRuntime/DafnyRuntime.csproj | ||
| dotnet build -f netstandard2.0 Source/DafnyRuntime/DafnyRuntime.csproj |
There was a problem hiding this comment.
Does this generate 3 runtimes?
There was a problem hiding this comment.
Yeah, one for each of those frameworks, so that folks downloading from NuGet can get the one that works for them. My understanding is that this is the best way to make .NET libraries available for many versions, but I'd love to hear about a better way if there is one.
.github/workflows/msbuild.yml
Outdated
| run: dotnet build Source/Dafny.sln | ||
| run: | | ||
| dotnet build Source/Dafny.sln | ||
| dotnet build -f net462 Source/DafnyRuntime/DafnyRuntime.csproj |
There was a problem hiding this comment.
Are these useful frameworks to target? Who would consume a netstandard2.0 or a net462 library? How about only targeting net5.0 or net3.1 depending on how far back we want to support?
There was a problem hiding this comment.
This was partly informed by the dependencies here with the adjustment that the current runtime doesn't build with net452 but does work as far back as netstandard2.0. I also took guidance from here.
There was a problem hiding this comment.
If Standard allows sharing code with Framework and Core, then why would you build for Standard AND something else?
From the linked docs:
Most widely used libraries will multi-target for both .NET Standard 2.0 and .NET 5+. Supporting .NET Standard 2.0 gives you the most reach, while supporting .NET 5+ ensures you can leverage the latest platform features for customers that are already on .NET 5+.
I think targeting just standard would be enough for us.
There was a problem hiding this comment.
Hmm. Re-reading that page, I think you may be right. It seems as though if we built for netstandard2.1 we might also need a separate build to support Framework (e.g., net462), but if we build for netstandard2.0 we don't need that?
There was a problem hiding this comment.
Yes, looks like it. But pff, that 2.1 vs 2.0 matters so much is confusing!
It seems that netstandard2.0 is sufficient
keyboardDrummer
approved these changes
Sep 1, 2022
keyboardDrummer
added a commit
to keyboardDrummer/dafny
that referenced
this pull request
Sep 8, 2022
This reverts commit 709ed5a.
keyboardDrummer
added a commit
that referenced
this pull request
Sep 8, 2022
This reverts commit 709ed5a. (PR #2604) Resolving the issue that Rider no longer builds: ``` Build started 09/08/2022 10:58:29. Logging verbosity is set to: Normal. 1>Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" on node 1 (build target(s)). 1>BuildDafnyRuntimeJar: Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar... ./gradlew -q build GenerateTargetFrameworkMonikerAttribute: Skipping target "GenerateTargetFrameworkMonikerAttribute" because all output files are up-to-date with respect to the input files. CoreCompile: Skipping target "CoreCompile" because all output files are up-to-date with respect to the input files. _CopyOutOfDateSourceItemsToOutputDirectory: Skipping target "_CopyOutOfDateSourceItemsToOutputDirectory" because all output files are up-to-date with respect to the input files. _CopyOutOfDateSourceItemsToOutputDirectoryAlways: Copying file from "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.cs" to "/Users/rwillems/Documents/SourceCode/dafny/Binaries/net6.0/DafnyRuntime.cs". GenerateBuildDependencyFile: Skipping target "GenerateBuildDependencyFile" because all output files are up-to-date with respect to the input files. CopyFilesToOutputDirectory: DafnyRuntime -> /Users/rwillems/Documents/SourceCode/dafny/Binaries/net6.0/DafnyRuntime.dll 1>Done Building Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (build target(s)). 1:2>Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" on node 1 (Pack target(s)). 1:2>Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (1:2) is building "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (1:9) on node 1 (_GetFrameworkAssemblyReferences target(s)). 1>BuildDafnyRuntimeJar: Compiling DafnyRuntimeJava to DafnyRuntimeJava/build/libs/DafnyRuntime.jar... ./gradlew -q build 1>Done Building Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (_GetFrameworkAssemblyReferences target(s)). 1:2>Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (1:2) is building "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (1:10) on node 1 (_GetFrameworkAssemblyReferences target(s)). 1>/usr/local/share/dotnet/sdk/6.0.201/Sdks/Microsoft.NET.Sdk/targets/Microsoft.PackageDependencyResolution.targets(267,5): error NETSDK1005: Assets file '/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/obj/project.assets.json' doesn't have a target for 'netstandard2.0'. Ensure that restore has run and that you have included 'netstandard2.0' in the TargetFrameworks for your project. 1>Done Building Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (_GetFrameworkAssemblyReferences target(s)) -- FAILED. 1>Done Building Project "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (Pack target(s)) -- FAILED. Build FAILED. "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (Pack target) (1:2) -> "/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/DafnyRuntime.csproj" (_GetFrameworkAssemblyReferences target) (1:10) -> (ResolvePackageAssets target) -> /usr/local/share/dotnet/sdk/6.0.201/Sdks/Microsoft.NET.Sdk/targets/Microsoft.PackageDependencyResolution.targets(267,5): error NETSDK1005: Assets file '/Users/rwillems/Documents/SourceCode/dafny/Source/DafnyRuntime/obj/project.assets.json' doesn't have a target for 'netstandard2.0'. Ensure that restore has run and that you have included 'netstandard2.0' in the TargetFrameworks for your project. ``` I've reproduced this issue on a fresh Dafny checkout. <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <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>
robin-aws
added a commit
that referenced
this pull request
Nov 17, 2022
…2795) Fixes #2779. Another attempt after the previous attempt (#2604) had to be reverted (#2710). I tried this with a fresh clone and didn't run into the Rider problem described in #2710 - I'm relatively confident the `<TargetFramework>net6.0</TargetFramework>` I've removed from `Directory.Build.props` was to blame, and/or just needing to thoroughly clean `bin` and `obj` directories. Note that I am partially relying on post-hoc testing of the nightly build packages after this is merged, to ensure the `net452` build actually works on Windows. Note also that the packaging warnings I refer to in one of the commit messages are an existing, orthogonal issue: #3069 <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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Allow the
DafnyRuntimepackage to work withnetstandard2.0andnet462, as well as the previousnet6.0. This should make Dafny target code that links with a pre-builtDafnyRuntime.dllmore portable.Fixes #2481
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.