Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

DafnyRuntime not compatible with .NET frameworks earlier than .NET 6.0 #2779

Closed
robin-aws opened this issue Sep 21, 2022 · 9 comments · Fixed by #2795
Closed

DafnyRuntime not compatible with .NET frameworks earlier than .NET 6.0 #2779

robin-aws opened this issue Sep 21, 2022 · 9 comments · Fixed by #2795
Assignees
@robin-aws
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c# Dafny's C# transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)

Comments

@robin-aws
Copy link
Member

Result of being too restrictive in the DafnyRuntime.csproj configuration. Blocks adoption by projects that need to support earlier versions such as https://github.com/aws/aws-encryption-sdk-dafny.
@robin-aws robin-aws added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant) lang: c# Dafny's C# transpiler and its runtime labels Sep 21, 2022
@robin-aws robin-aws self-assigned this Sep 21, 2022
@robin-aws robin-aws added the release-blocker Must be resolved before the next release label Sep 21, 2022
@robin-aws
Copy link
Member Author

Abusing release-blocker a bit just to make sure this is fixed (if possible) before the next release, which should happen very soon to address #2776.

@atomb
Copy link
Member

atomb commented Sep 21, 2022

I believe this was resolved by #2604. It uses a slightly different set of target frameworks than https://github.com/aws/aws-encryption-sdk-dafny, but my understanding is that it's a compatible set.

@seebees
Copy link

seebees commented Sep 22, 2022

@atomb I'm not sure either. But I think we need to add net452 as well. There are some strange edge cases in .net where core, framework, and net are somehow not all the same.

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Sep 22, 2022 •
edited
Loading

I believe this was resolved by #2604. It uses a slightly different set of target frameworks than https://github.com/aws/aws-encryption-sdk-dafny, but my understanding is that it's a compatible set.

Note that #2604 was reverted: #2710

@robin-aws robin-aws mentioned this issue Sep 23, 2022
Merged
@MikaelMayer MikaelMayer removed the release-blocker Must be resolved before the next release label Sep 30, 2022
robin-aws added a commit that referenced this issue Nov 17, 2022
@robin-aws
Build DafnyRuntime for netstandard2.0 and net452 instead of net6.0 (#…
ca741e9 
…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>
@texastony
Copy link

Was this closed on the PR merge or a release of the Runtime to nuget?
It would appear on the PR merge, as Nuget is still restricting: https://www.nuget.org/packages/DafnyRuntime#supportedframeworks-body-tab

@robin-aws
Copy link
Member Author

On the PR merge, but we are already working towards getting a release out in a matter of days.

@texastony
Copy link

On November 26th,
I pulled DafnyRuntime @ 3.9.1.41027-nightly-2022-11-26-2e0b8a9
into a project and attempted a build with following .csproj settings:

<LangVersion>7.3</LangVersion>
<TargetFrameworks>netstandard2.1;net452</TargetFrameworks>

Running dotnet build resulted in Error,
due to the implicit use of System.Globalization @ 4.3.0 by DafnyRuntime,
which does not support C# 7.3.

Sample Error:

  STD.GlobalUsings.g.cs(2, 1): [CS8370] Feature 'global using directive' is not available in C# 7.3. Please use language version 10.0 or greater.

I can do more digging, but it appears that DafnyRuntime does not support C# @ 7.3.

@texastony
Copy link

texastony commented Nov 26, 2022 •
edited
Loading

Using C# @ 10, I encountered another error,
though it MAY not be from DafnyRuntime:

net452/STD.GlobalUsings.g.cs(6,33): error CS0234: The type or namespace name 'Http' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)

I can work around this by adding System.Net.Http as a dependency:

<PackageReference Include="System.Net.Http" Version="4.3.4" />

With that, my project builds for Frameworks netstandard2.1;net452.

Again,
I am not certain if the root cause of the net issue is the DafnyRuntime or
MSFT's System.Globalization not declaring a dependency on System.Net.Http.

@texastony
Copy link

Ahh... I a may have been too quick to speak.
It turns out that I had:

    <ImplicitUsings>enable</ImplicitUsings>

in my csproj.
If I disable that, then I can compile with 7.3 and no dependency on System.Net.Http or System.Globalization.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robin-aws robin-aws

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny lang: c# Dafny's C# transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Build DafnyRuntime for netstandard2.0 and net452 instead of net6.0 robin-aws/dafny
6 participants
@atomb @seebees @keyboardDrummer @MikaelMayer @texastony @robin-aws