Feat: Translate Dafny tests to Rust tests #5676
Conversation
This PR detects all tests and creates adequate equivalent Rust tests in the same file, by calling methods via top-level functions and translating `{:test}` attributes to the equivalent `#[test]` in Rust.
Moreover, it translates the `{:test}` annotation on modules to the equivalent `#[cfg(test)]` in Rust, so that it makes it possible to exclude entire modules when not in test mode.
I wrote a test that verifies that tests can be executed and that the resulting source code emits `#[cfg(test)]`
There was a problem hiding this comment.
Good feature to have, just some suggestions on packaging.
I do still feel it should be possible for the --include-test-runner approach to work for Rust eventually too, we just need to go deeper into the Rust kernel to use what ever panic recovery cargo test itself uses, so I'm trying not to close that door now.
docs/dev/news/5666.feat
Outdated
| if HasTestAttribute(mod.attributes) { | ||
| attributes := [R.RawAttribute("#[cfg(test)]")]; | ||
| } |
There was a problem hiding this comment.
I'd rather not do exactly this because it's not a complete solution. {:test} on modules doesn't have any meaning at the Dafny level as it does for methods. And it's likely to be misinterpreted as "This scope contains test methods" as it is in some testing frameworks, rather than "This code should only be compiled in test mode". I suspect users won't realize they have to also put {:test} on helper modules as well.
If you really want this I'd suggest {:rust_test_cfg} or something like that instead.
There was a problem hiding this comment.
I'll go with {:rust_cfg_test} then, it will be easier later to have Backend-specific typed options.
There was a problem hiding this comment.
I also updated the docs to mention the two attributes in the Rust-specific section.
| @@ -2084,6 +2093,27 @@ module {:extern "DCOMP"} DafnyToRustCompiler { | |||
| ); | |||
| s := s + [R.ImplDecl(i)]; | |||
| } | |||
| // Add test methods | |||
There was a problem hiding this comment.
We should only do this if the RunAllTestsMainMethod.IncludeTestRunner option is off - we already do that for C#: https://github.com/dafny-lang/dafny/blob/master/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs#L3454
The two ways of implementing {:test} conflict subtley.
There was a problem hiding this comment.
I understand that it might be necessary for C# for some reason, but I don't see a reason to do that in Rust.
Currently "dafny test" is the only command that forces to turn on this option because that way it won't create test fixtures, just run them regularly.
However, in the future, "dafny test" for Rust should not include the Test Runner but call "cargo test" instead, so it should safely ignore this IncludeTestRunner.
That is, unless you have another explanation about why it is needed?
There was a problem hiding this comment.
I'm not sure I'd want to make dafny test call cargo test instead, since the output will be different from the other backends.
But on second look I don't think it's harmful to add #[test] even if you're running the common test runner, so I won't object to leaving it in for simplicity.
A bit more exciting than an empty file
…dafny into feat-5666-cargo-test
docs/dev/news/5666.feat
Outdated
There was a problem hiding this comment.
LGTM, but just noticed the PR number in the file name is wrong.
Co-authored-by: Robin Salkeld <[email protected]>
This PR detects all tests and creates adequate equivalent Rust tests in the same file, by calling methods via top-level functions and translating
{:test}attributes to the equivalent#[test]in Rust. Moreover, it translates the{:test}annotation on modules to the equivalent#[cfg(test)]in Rust, so that it makes it possible to exclude entire modules when not in test mode.I wrote a test that verifies that tests can be executed and that the resulting source code emits
#[cfg(test)]By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.