feat: add the Errata test framework - #956
Open
david-christiansen wants to merge 31 commits into
Open
Conversation
Errata is a test framework, designed to be something we can extract to its own repo after we get some experience with it here (so it can be used e.g. in verso-slides and lean-sqlite). In Errata, tests are marked by the `@[test]` attribute. Their docstring and source range are saved for failure reporting. The value of a test can have any type with an `IsTest` instance. Some machinery in the Lakefile enumerates all tests, providing them to the runner. Elaboration-time tests can also be implemented using `#test_msgs` and `#test_guard`, which are versions of `#guard_msgs` and `#guard` that run the compile-time test but save the result as a test case for reporting together with the rest of the tests. Errata also supports saving JUnit XML, which various GitHub actions can conveniently display for us.
Migrate command-line parsing to Cli and improve verbosity settings RE success/failure
The update path replaces the recorded tree wholesale, so a path that changed shape between file and directory no longer makes the update run throw an IO error.
Dangling bytes at the end of a failing test no longer replace the message with one about byte encodings.
Text writes go through the same pending-byte pathway as raw writes, so a print no longer overtakes an earlier raw write that is waiting for the rest of its code point.
assertTrue now takes an optional detail like the other assertions, so predicate checks can attach the value that failed them. assertThrowsIO expects an action to throw an IO.Error, with a predicate picking the subset of acceptable errors.
This allows warnings such as "unused parameter" to fail in CI.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Errata is a test framework, designed to be something we can extract to its own repo after we get some experience with it here (so it can be used e.g. in verso-slides and lean-sqlite).
In Errata, tests are marked by the
@[test]attribute. Their docstring and source range are saved for failure reporting. The value of a test can have any type with anIsTestinstance. Some machinery in the Lakefile enumerates all tests, providing them to the runner.Elaboration-time tests can also be implemented using
#test_msgsand#test_guard, which are versions of#guard_msgsand#guardthat run the compile-time test but save the result as a test case for reporting together with the rest of the tests.Errata also supports saving JUnit XML, which various GitHub actions can conveniently display for us.