From a1972766de5c0d53e8ce3e8cc19e63becb68871a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Tue, 25 Jun 2024 10:37:37 -0500
Subject: [PATCH] Chore: Internal backends should not fail CI (#5573)

Until the Rust code generator is finished, we shouldn't block everyone
else's work by requiring .rs.check files or even update them every time,
since the process is manual and very lengthy

This does not remove the execution of the Rust compiler, only remove the
check, so that we still have some kind of coverage. Also, we display
non-blocking error messages.
However, this might kill the meta-tests, I'll see how to fix that.

<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>
---
 ...stentCompilerBehavior.dfy.testdafny.expect |  1 +
 ...tBeyondVerifierExpect.dfy.testdafny.expect |  1 +
 Source/TestDafny/MultiBackendTest.cs          | 22 +++++++++++++++++++
 3 files changed, 24 insertions(+)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
index 2bd757b626..7e24d9e430 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/InconsistentCompilerBehavior.dfy.testdafny.expect
@@ -50,4 +50,5 @@ Diff (changing expected into actual):
 +0
  
 
+(non-blocking) The Rust code generator is internal. Not having a '*.rs.check' file is acceptable for now.
 Executing on ResolvedDesugaredExecutableDafny...
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect
index ce5735dda4..a881545e3b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.testdafny.expect
@@ -50,4 +50,5 @@ Diff (changing expected into actual):
 +hello
  
 
+(non-blocking) The Rust code generator is internal. Not having a '*.rs.check' file is acceptable for now.
 Executing on ResolvedDesugaredExecutableDafny...
diff --git a/Source/TestDafny/MultiBackendTest.cs b/Source/TestDafny/MultiBackendTest.cs
index cbc2996835..6e9d6272ff 100644
--- a/Source/TestDafny/MultiBackendTest.cs
+++ b/Source/TestDafny/MultiBackendTest.cs
@@ -423,6 +423,12 @@ await output.WriteLineAsync(
       }
 
       await output.WriteLineAsync(diffMessage);
+      if (backend.IsInternal) {
+        await output.WriteLineAsync(
+          $"(non-blocking) The {backend.TargetName} code generator is internal. Not having a '*.{backend.TargetId}.check' file is acceptable for now.");
+        return 0;
+      }
+
       return 1;
     }
 
@@ -456,9 +462,25 @@ await output.WriteLineAsync(
         }
       }
 
+      if (backend.IsInternal && checkResult != 0) {
+        await output.WriteLineAsync(
+          $"(non-blocking) The {backend.TargetName} code generator is internal. An unmatched '*.{backend.TargetId}.check' file is acceptable for now.");
+        return 0;
+      }
+
       return checkResult;
     }
 
+
+    if (backend.IsInternal) {
+      await output.WriteLineAsync($"(non-blocking) Execution failed for the internal {backend.TargetName} code generator, for reasons other than known unsupported features. Output:");
+      await output.WriteLineAsync(outputString);
+      await output.WriteLineAsync("Error:");
+      await output.WriteLineAsync(error);
+      await output.WriteLineAsync(
+        $"The {backend.TargetName} code generator is internal. An unmatched '*.{backend.TargetId}.check' file is acceptable for now.");
+      return 0;
+    }
     await output.WriteLineAsync("Execution failed, for reasons other than known unsupported features. Output:");
     await output.WriteLineAsync(outputString);
     await output.WriteLineAsync("Error:");