ci: Fix nightly build tests broken by skipping Rust (#5566)

A couple of metatests are broken by temporarily skipping the rust
backend in the nightly build only. This change fixes that by adding a
`--compilers` flag to `%testDafnyForEachCompiler` that overrides the
`DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS` environment variable, so those
tests can work consistently.

Also tweaked `run-deep-tests` to set
`DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS` just as the nightly build does
so this kind of problem should show up consistently if it happens again.

.github/workflows/msbuild.yml

@@ -76,6 +76,8 @@ jobs:
       # This is the best way to fix an issue in master that was only caught by the nightly build.
       all_platforms: ${{ contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')}}
       num_shards: 5
+      # Omit Rust in the nightly build (or rather simulating it here) because Rust is known to have random issues
+      compilers: ${{ (contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.push.labels.*.name, 'run-deep-tests')) && 'cs,java,go,js,cpp,dfy,py' || '' }}
 
   test-coverage-analysis:
     runs-on: ubuntu-20.04

Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy

@@ -1,4 +1,7 @@
-// RUN: ! %testDafnyForEachCompiler --refresh-exit-code=0 "%s" > "%t"
+// Note we specify the set of compilers to test explicitly since we're looking at the actual output,
+// and otherwise using DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS breaks this test.
+
+// RUN: ! %testDafnyForEachCompiler --refresh-exit-code=0 --compilers cs,java,go,js,cpp,dfy,py,rs "%s" > "%t"
 // RUN: %diff "%s.testdafny.expect" "%t"
 
 // A %testdafny test case expected to fail, since the given

Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy

@@ -1,4 +1,7 @@
-// RUN: ! %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --allow-warnings > "%t"
+// Note we specify the set of compilers to test explicitly since we're looking at the actual output,
+// and otherwise using DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS breaks this test.
+
+// RUN: ! %testDafnyForEachCompiler --refresh-exit-code=0 --compilers cs,java,go,js,cpp,dfy,py,rs "%s" -- --allow-warnings > "%t"
 // RUN: %diff "%s.testdafny.expect" "%t"
 
 method Main() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect

@@ -1 +1 @@
-TestBeyondVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
+TestBeyondVerifierExpect.dfy(9,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.

Source/TestDafny/MultiBackendTest.cs

@@ -24,6 +24,9 @@ public class ForEachCompilerOptions {
 
   [Option("refresh-exit-code", HelpText = "If present, also run with --type-system-refresh and expect the given exit code.")]
   public int? RefreshExitCode { get; set; } = null;
+
+  [Option("compilers", HelpText = "Test on only the given compilers.")]
+  public string? Compilers { get; set; } = null;
 }
 
 [Verb("features", HelpText = "Print the Markdown content documenting feature support for each compiler.")]
@@ -57,10 +60,6 @@ public class MultiBackendTest {
   private readonly TextWriter output;
   private readonly TextWriter errorWriter;
 
-  private static readonly string[] CompilerFilter =
-    (Environment.GetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS") ?? "")
-    .Split(",")
-    .Where(name => name.Trim() != "").ToArray();
   private static readonly string? IntegrationTestsRootDir =
     Environment.GetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_ROOT_DIR");
   private static readonly bool UpdateTargetExpectFile = DiffCommand.UpdateExpectFile;
@@ -109,6 +108,14 @@ private async Task<int> ForEachCompiler(ForEachCompilerOptions options) {
     var pluginArguments = pluginParseResult.GetValueForOption(CommonOptionBag.PluginOption);
     var plugins = DafnyOptions.ComputePlugins(new List<Plugin>(), pluginArguments ?? new List<string>());
 
+    string rawCompilerFilter = options.Compilers ??
+                               Environment.GetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_ONLY_COMPILERS")
+                               ?? "";
+    string[] CompilerFilter = rawCompilerFilter
+      .Split(",")
+      .Where(name => name.Trim() != "").ToArray();
+
+
     // First verify the file (and assume that verification should be successful).
     // Older versions of test files that now use %testDafnyForEachCompiler were sensitive to the number
     // of verification conditions (i.e. the X in "Dafny program verifier finished with X verified, 0 errors"),