Convert test infrastructure to tasty-golden based testsuite

DEVELOPER.md

@@ -0,0 +1,87 @@
+# Developer Documentation
+
+## Running the Test Suite
+
+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 `.hs` files are the golden values.
+- **Fail tests** (`test/Fail/`): Agda files that should fail to compile. The error messages (in `.err` files) are the golden values.
+
+### Running All Tests
+
+```bash
+# Run all tests (includes whitespace check and container tests)
+make test
+
+# Or run just the agda2hs tests
+cabal test agda2hs-test
+```
+
+### Running Specific Test Categories
+
+```bash
+# 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'
+```
+
+### Running Individual Tests
+
+```bash
+# 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/'
+```
+
+## Updating Golden Values
+
+When you make changes that intentionally affect the test output, you need to update the golden values:
+
+```bash
+# 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.
+
+## Adding New Tests
+
+### Adding a Succeed Test
+
+1. Create a new `.agda` file in `test/Succeed/`
+2. Run `make golden-succeed` to generate the golden `.hs` file
+3. Verify the generated Haskell code is correct
+4. Commit both the `.agda` and `.hs` files
+
+### Adding a Fail Test
+
+1. Create a new `.agda` file in `test/Fail/`
+2. Run `make golden-fail` to generate the golden `.err` file
+3. Verify the error message is correct
+4. Commit both the `.agda` and `.err` files
+
+## Test Ordering
+
+Tests are ordered by:
+1. Modification date of the `.agda` file (newest first)
+2. Modification date of the golden value file (newest first)
+3. 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.

LICENSE

@@ -1,4 +1,4 @@
-Copyright 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus.
+Copyright 2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
 

Makefile

@@ -1,55 +1,63 @@
-.PHONY : install agda repl libHtml testContainers test test-on-CI testHtml golden clean docs
+.PHONY : build install agda repl libHtml testContainers test succeed fail golden golden-succeed golden-fail clean docs fixWhitespace checkWhitespace
+
 FILES = $(shell find src -type f)
 
 build :
-	cabal build
+cabal build
 
 install :
-	cabal install --overwrite-policy=always
+cabal install --overwrite-policy=always
 
 agda :
-	cabal install Agda --program-suffix=-erased --overwrite-policy=always
+cabal install Agda --program-suffix=-erased --overwrite-policy=always
 
 repl :
-	cabal repl # e.g. `:set args -itest -otest/build test/AllTests.agda ... main ... :r ... main`
+cabal repl
 
 libHtml :
-	cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
-	cp html/Haskell.Prelude.html html/index.html
-
-test/agda2hs : $(FILES)
-	cabal install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
+cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
+cp html/Haskell.Prelude.html html/index.html
 
 testContainers:
-	cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
+
+# Run all tests
+test : checkWhitespace succeed fail testContainers
+
+# Run only successful tests
+succeed :
+cabal test agda2hs-test --test-options='-p Succeed'
 
-test : checkWhitespace test-on-CI
+# Run only failing tests
+fail :
+cabal test agda2hs-test --test-options='-p Fail'
 
-test-on-CI : test/agda2hs testContainers
-	make -C test
+# Update all golden values
+golden : golden-succeed golden-fail
 
-testHtml : test/agda2hs
-	make -C test html
+# Update golden values for successful tests
+golden-succeed :
+cabal test agda2hs-test --test-options='-p Succeed --accept'
 
-golden :
-	make -C test golden
+# Update golden values for failing tests
+golden-fail :
+cabal test agda2hs-test --test-options='-p Fail --accept'
 
 clean :
-	make -C test clean
+cabal clean
+rm -rf test/_build/
 
 docs :
-	make -C docs html
+make -C docs html
 
 FIXW_BIN = fix-whitespace
 
-.PHONY : fixWhitespace ## Fix the whitespace issue.
 fixWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
-	$(FIXW_BIN)
+$(FIXW_BIN)
 
-.PHONY : checkWhitespace ## Check the whitespace issue without fixing it.
 checkWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
-	$(FIXW_BIN) --check
+$(FIXW_BIN) --check
 
-.PHONY : have-bin-% ## Installing binaries for developer services
+.PHONY : have-bin-%
 have-bin-% :
-	@($* --help > /dev/null) || $(CABAL) install --ignore-project $*
+@($* --help > /dev/null) || $(CABAL) install --ignore-project $*

agda2hs.cabal

@@ -3,9 +3,9 @@ name:                agda2hs
 version:             1.5
 license:             BSD-3-Clause
 license-file:        LICENSE
-author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus
+author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
 maintainer:          jesper@sikanda.be
-copyright:           2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, and Heinrich Apfelmus
+copyright:           2025 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, Jakob Naucke, Heinrich Apfelmus, Andreas Abel, and Copilot
 category:            Language, Compiler
 build-type:          Simple
 synopsis:            Compiling Agda code to readable Haskell.
@@ -21,6 +21,14 @@ extra-doc-files:    CHANGELOG.md
 data-files:
     lib/base/base.agda-lib
     lib/base/**/*.agda
+    test/agda2hs-test.agda-lib
+    test/Haskell/**/*.agda
+    test/Succeed/*.agda
+    test/Succeed/*.hs
+    test/Succeed/**/*.agda
+    test/Succeed/**/*.hs
+    test/Fail/*.agda
+    test/Fail/*.err
 
 source-repository head
   type:     git
@@ -83,3 +91,22 @@ executable agda2hs
                        NondecreasingIndentation
                        OverloadedStrings
   ghc-options:         -Werror -rtsopts
+
+test-suite agda2hs-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Main.hs
+  build-depends:       base                 >= 4.13    && < 4.22,
+                       bytestring           >= 0.11.5  && < 0.13,
+                       directory            >= 1.2.6.2 && < 1.4,
+                       filepath             >= 1.4.1.0 && < 1.6,
+                       process              >= 1.6     && < 1.7,
+                       tasty                >= 1.4     && < 1.6,
+                       tasty-golden         >= 2.3     && < 2.4,
+                       text                 >= 2.0.2   && < 2.2,
+                       time                 >= 1.9     && < 1.15,
+  default-language:    Haskell2010
+  default-extensions:  OverloadedStrings
+                       ScopedTypeVariables
+  build-tool-depends:  agda2hs:agda2hs
+  ghc-options:         -threaded