Use Dafny tooling instead of lit to verify/test

[robin-aws]

(pulling a discussion from the original first big PR out: https://github.com/dafny-lang/libraries/pull/7#discussion_r680374440)

Besides what @samuelgruetter is saying about testing that pre- and post-conditions make sense, I want the CI to ensure the code can be compiled and run and produce the right results. Given that there are lots of function methods in this library and not just functions, it should be a requirement to ensure that the code is actually compilable and works correctly.

Here's a really simple example:

module SeqTest {
  import Seq
  method {:test} TestApply() {
    var input := [1, 2, 3, 4, 5];
    var output := Seq.apply(i => i * 2, input);
    expect output == [2, 4, 6, 8, 10];
  }
}

Building and testing would be a two step process:

dafny /compile:0 /spillTargetCode:2 <all Dafny source files>

That will still run verification on all the source files and potentially fail. If verification succeeds, you would then execute the resulting C# tests:

dotnet test

This would require a .csproj file similar to the one used in the Dafny test suite: https://github.com/dafny-lang/dafny/blob/master/Test/DafnyTests/DafnyTests.csproj.

The {:test} attribute is only handled by the C# compiler for now but we're adding support for the other target languages. Plus, as I mentioned in https://github.com/dafny-lang/dafny/issues/1322#issuecomment-889184653, we should make the process a single simple step by adding something like a dafny test command.

Note that this implies dropping the lit tool for verifying and testing this library. lit is a great tool for testing compilers or CLI tools themselves, but it's a poor match for end-user programs using such tools. We shouldn't expect any of this code to fail to verify or compile, so we don't need the ability to assert the exact expected error/warning behavior. This project can instead serve as an example for best practices in maintaining Dafny code, which should only involve verifying, compiling, and running Dafny code.

Dropping lit will mean that we need to change the solution we set up for testing this package in the CI of the dafny-lang/dafny repo, but that is definitely doable, and can be handled at the same time that we update the submodule pointer to pick up the new version without lit header commands in all the Dafny files.

[cpitclaudel]

Note that this implies dropping the lit tool for verifying and testing this library.

? Don't our compiler tests use lit currently? It seems fine for this purpose.

[robin-aws]

Lit is great for testing compilers, but this repository is not a compiler. :)

[prvshah51]

I think, we will also have more control with warnings as we will not have to match the output of the file but just verify/compile or can also consider warnings as errors if needed.

[keyboardDrummer]

With the /runAllTests option and the upcoming test command (https://github.com/dafny-lang/dafny/pull/3054), this issue seems obsolete. Is there remaining work to be done in libraries @robin-aws ?

[robin-aws]

Not obsolete, it's just that as you say there are other, probably better alternatives to the setup I originally described. We should still replace lit with either /runAllTests or dafny test.

[davidcok]

1) The checks that library code verifies sometimes need to customize options (e.g. --disable-nonlinear-arithmetic) to files being verified, and perhaps check verification with more than one set of options. This seems to be a good fit to lit and not to {:test}.

2) We also need checks that code calling the library can be verified, establishing that the specs of the library routines are usable. These could be separate test files (in a Tests folder, say) or they could be bundled into the library files themselves at the rist of bloating both the text of the files and the executables that use the files. Also a good fit to lit.

3) And we should have dynamic tests of the functionality. These also could be in separate Test file or bundled into the library files, and would use {:test} -- and would have the same tradeoff between locality and bloat as item (2).

[robin-aws]

@davidcok My general argument is that yes, lit is definitely powerful enough to cover all the use cases we need, but because it's so general it's much less easy to use for Dafny end users. I say that Dafny codebases deserve their own fit-to-purpose build system, and by having all of these libraries use Dafny ecosystem features we'll help ensure those features are also good enough for other projects.

We're not there yet, so I don't object to small improvements to the lit-based setup in the meantime. But I don't want to settle for lit as the permanent solution and copy over tons of the machinery we have in dafny-lang/dafny (which lit IS a great fit for testing) to make it work well enough in the long term: we shouldn't require other Dafny projects to do the same. I'd much rather spend the effort in making Dafny tooling good enough for these use cases instead.

To some of your points:

1. I think that's more an argument for grouping files together into logical projects with common configuration, and/or using the per module {:options} feature.

2. Agreed it would be better to separate source and test files somehow. So far we have examples separate from src, but I'd probably prefer to have examples/tests sitting next to, but not distributed with, the source files they relate to. It's definitely possible to support this, for example see the src and test directories here: https://github.com/aws/aws-encryption-sdk-dafny.