Always generate _Test__Main_

[ajewellamz]

Summary

Test__Main should be generated from translate as well as test

Background and Motivation

Sometimes a person wants to do some testing or instrumentation, and needs to get at an entry point that runs all the tests. Test__Main is that entry point, and so it should be more widely available.

Proposed Feature

In Rust, or possibly all languages, dafny translate should generate the same Test__Main function as dafny test.
The only difference between the two outputs would then be that dafny test creates a main() where dafny translate does not.

Alternatives

No response

[keyboardDrummer]

Have you looked at the --include-test-runner option that's part of all the dafny translate commands?