Skip to content

Commit

Permalink
Chore: Internal backends should not fail CI (#5573)
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
MikaelMayer authored Jun 25, 2024
1 parent 2e866ef commit a197276
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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...
Original file line number Diff line number Diff line change
Expand Up @@ -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...
22 changes: 22 additions & 0 deletions Source/TestDafny/MultiBackendTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down Expand Up @@ -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:");
Expand Down

0 comments on commit a197276

Please sign in to comment.