Build DafnyRuntime for netstandard2.0 and net452 instead of net6.0 (#…

…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>

Scripts/package.py

@@ -127,21 +127,23 @@ def zipify_path(fpath):
         """Zip entries always use '/' as the path separator."""
         return fpath.replace(os.path.sep, '/')
 
-    def run_publish(self, project):
+    def run_publish(self, project, framework = None):
         env = dict(os.environ)
         env["RUNTIME_IDENTIFIER"] = self.target
         flush("   + Publishing " + project)
         remaining = 3
         exitStatus = 1
         while 0 < remaining and exitStatus != 0:
             remaining -= 1
+            otherArgs = []
+            if framework:
+                otherArgs += ["-f", framework]
             exitStatus = subprocess.call(["dotnet", "publish", path.join(SOURCE_DIRECTORY, project, project + ".csproj"),
                 "--nologo",
-                "-f", "net6.0",
                 "-o", self.buildDirectory,
                 "-r", self.target,
                 "--self-contained",
-                "-c", "Release"], env=env)
+                "-c", "Release"] + otherArgs, env=env)
             if exitStatus != 0:
                 if remaining == 0:
                     flush("failed! (Is Dafny or the Dafny server running?)")
@@ -160,7 +162,8 @@ def build(self):
         run(["make", "--quiet", "clean"])
         self.run_publish("DafnyLanguageServer")
         self.run_publish("DafnyServer")
-        self.run_publish("DafnyRuntime")
+        self.run_publish("DafnyRuntime", "netstandard2.0")
+        self.run_publish("DafnyRuntime", "net452")
         self.run_publish("Dafny")
 
     def pack(self):

Source/DafnyCore/Compilers/Compiler-Csharp.cs

@@ -3170,6 +3170,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       var libPath = Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location);
       if (DafnyOptions.O.UseRuntimeLib) {
         compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Path.Join(libPath, "DafnyRuntime.dll")));
+        compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Assembly.Load("netstandard").Location));
       }
 
       var standardLibraries = new List<string>() {

Source/DafnyRuntime/DafnyRuntime.cs

@@ -890,7 +890,7 @@ public interface ISequence<out T> : IEnumerable<T> {
   }
 
   public abstract class Sequence<T> : ISequence<T> {
-    public static readonly ISequence<T> Empty = new ArraySequence<T>(Array.Empty<T>());
+    public static readonly ISequence<T> Empty = new ArraySequence<T>(new T[0]);
 
     private static readonly TypeDescriptor<ISequence<T>> _TYPE = new Dafny.TypeDescriptor<ISequence<T>>(Empty);
     public static TypeDescriptor<ISequence<T>> _TypeDescriptor() {
@@ -1187,7 +1187,8 @@ private ImmutableArray<T> ComputeElements() {
       // Traverse the tree formed by all descendants which are ConcatSequences
       var ansBuilder = ImmutableArray.CreateBuilder<T>(count);
       var toVisit = new Stack<ISequence<T>>();
-      var (leftBuffer, rightBuffer) = (left, right);
+      var leftBuffer = left;
+      var rightBuffer = right;
       if (left == null || right == null) {
         // elmts can't be .IsDefault while either left, or right are null
         return elmts;
@@ -1198,7 +1199,8 @@ private ImmutableArray<T> ComputeElements() {
       while (toVisit.Count != 0) {
         var seq = toVisit.Pop();
         if (seq is ConcatSequence<T> cs && cs.elmts.IsDefault) {
-          (leftBuffer, rightBuffer) = (cs.left, cs.right);
+          leftBuffer = cs.left;
+          rightBuffer = cs.right;
           if (cs.left == null || cs.right == null) {
             // !cs.elmts.IsDefault, due to concurrent enumeration
             toVisit.Push(cs);

Source/DafnyRuntime/DafnyRuntime.csproj

@@ -6,7 +6,7 @@
       <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
       <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
       <DefineConstants>TRACE;ISDAFNYRUNTIMELIB</DefineConstants>
-      <TargetFramework>net6.0</TargetFramework>
+      <TargetFrameworks>netstandard2.0;net452</TargetFrameworks>
       <OutputPath>..\..\Binaries\</OutputPath>
       <LangVersion>7.3</LangVersion>
       <PackageLicenseExpression>MIT</PackageLicenseExpression>

Source/Directory.Build.props

@@ -1,8 +1,6 @@
 <Project>
 
   <PropertyGroup>
-    <!-- Target framework -->
-    <TargetFramework>net6.0</TargetFramework>
     <VersionPrefix>3.9.1.41027<!--Version 3.9.1, year 2018+4, month 10, day 27.--></VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>

Test/comp/separate-compilation/Inputs/producer/TimesTwo.csproj

@@ -2,7 +2,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
     <PropertyGroup>
-        <TargetFramework>net6.0</TargetFramework>
+        <TargetFramework>netstandard2.0</TargetFramework>
     </PropertyGroup>
 
     <ItemGroup>