diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index 8d4e3b9d7e..2b1fc10479 100644 --- a/.github/workflows/msbuild.yml +++ b/.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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy index b7d4f29734..d0a9d5c633 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy index 75feb08efc..bda4fbd421 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy +++ b/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() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect index 2d8130bc48..14b278fe2e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect +++ b/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. diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs index 1eb4326e3f..f6680e4997 100644 --- a/Source/TestDafny/MultiBackendTest.cs +++ b/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 ForEachCompiler(ForEachCompilerOptions options) { var pluginArguments = pluginParseResult.GetValueForOption(CommonOptionBag.PluginOption); var plugins = DafnyOptions.ComputePlugins(new List(), pluginArguments ?? new List()); + 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"),