The test suite uses tasty-golden for golden value testing. Tests are organized into two categories:
- Succeed tests (
test/Succeed/): Agda files that should compile successfully with agda2hs. The generated.hsfiles are the golden values. - Fail tests (
test/Fail/): Agda files that should fail to compile. The error messages (in.errfiles) are the golden values.
# Run all tests (includes whitespace check and container tests)
make test
# Or run just the agda2hs tests
cabal test agda2hs-test# Run only successful tests
make succeed
# Run only failing tests
make fail
# Or using cabal directly with pattern matching
cabal test agda2hs-test --test-options='-p Succeed'
cabal test agda2hs-test --test-options='-p Fail'# Run a specific test by name
cabal test agda2hs-test --test-options='-p /Fixities/'
# Run tests matching a pattern
cabal test agda2hs-test --test-options='-p /Issue/'When you make changes that intentionally affect the test output, you need to update the golden values:
# Update all golden values
make golden
# Update only successful test golden values
make golden-succeed
# Update only failing test golden values
make golden-fail
# Or using cabal directly
cabal test agda2hs-test --test-options='--accept'After updating golden values, review the changes with git diff to ensure they are correct before committing.
- Create a new
.agdafile intest/Succeed/ - Run
make golden-succeedto generate the golden.hsfile - Verify the generated Haskell code is correct
- Commit both the
.agdaand.hsfiles
- Create a new
.agdafile intest/Fail/ - Run
make golden-failto generate the golden.errfile - Verify the error message is correct
- Commit both the
.agdaand.errfiles
Tests are ordered by:
- Modification date of the
.agdafile (newest first) - Modification date of the golden value file (newest first)
- Alphabetically
This ordering ensures that recently modified tests appear first in the output, making it easier to focus on tests you're actively working on.