-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Description
I think we want more flexible and ad-hoc solution to setting up regression tests that avoid blowing up the basil repository size with a lot of examples. My vague plan here is
- move examples to a separate repository and add as a submodule to BASIL repo https://github.com/UQ-PAC/basil-tests-regression
- add a small configuration for each test similar to the framework used in the boogie repo https://github.com/boogie-org/boogie/tree/master/Test/aitest0.
- for our purposes maybe a json file
{flags: ["--analyse", "--simplify"], expect: {"boogie": "expect.bpl"}}with options for much weaker requirements than our systemtests suite, e.g. ranging from non-crashing, boogie's typecheck and validation passing, to verification.
- for our purposes maybe a json file
It is then possible to bolt on the reproducible build work to this separate repository after the fact to manage building the examples reliably, but storing the examples separately reduces the need to keep checked-in sizes small.
Metadata
Metadata
Assignees
Labels
No labels