Convert test infrastructure to tasty-golden based testsuite (#450)

* Initial plan

* Convert test infrastructure to tasty-golden based testsuite

- Create test/Succeed/ and test/Fail/ directory structure
- Move .agda test files to appropriate directories
- Move golden .hs files next to their .agda files in test/Succeed/
- Move golden .err files next to their .agda files in test/Fail/
- Create test/Main.hs test runner using tasty-golden
- Add test-suite section to agda2hs.cabal
- Add test data files to cabal file
- Remove old AllTests.agda, AllFailTests.agda, AllCubicalTests.agda
- Remove old golden/ directory

Co-authored-by: andreasabel <[email protected]>

* Fix test runner for module discovery and UTF-8 encoding

- Add include paths for agda2hs to find modules in Succeed directory
- Add include paths for GHC to find imported Haskell modules
- Fix UTF-8 encoding issue in error message comparison using Data.Text
- Add text dependency to test-suite
- Revert agda-lib changes (no longer needed with include path approach)
- Remove duplicate Cubical subdirectory

Co-authored-by: andreasabel <[email protected]>

* Convert test infrastructure to tasty-golden based testsuite

- Create test/Succeed/ and test/Fail/ directory structure
- Move .agda test files with golden values alongside (.hs and .err)
- Create test/Main.hs test runner using tasty-golden
- Add test-suite section to agda2hs.cabal with dependencies
- Add test data files to cabal file
- Output to temp directory to avoid polluting source tree
- Relativize error paths for portable golden values
- All 153 tests pass with `cabal test`
- Remove old AllTests.agda, AllFailTests.agda, AllCubicalTests.agda
- Remove old golden/ directory

Co-authored-by: andreasabel <[email protected]>

* Address PR review feedback

- Move language extensions to default-extensions in cabal file
- Use System.Directory.doesDirectoryExist instead of custom implementation
- Use Data.List.isInfixOf instead of custom implementation
- Inline content read and add comment about golden value
- Sort files by modification time (newest first), then golden value time, then alphabetically
- Update Makefile with new test goals (succeed, fail, golden, golden-succeed, golden-fail)
- Delete test/Makefile
- Add DEVELOPER.md with test suite documentation
- Add Andreas Abel and Copilot to author lists in .cabal and LICENSE

Co-authored-by: andreasabel <[email protected]>

* Remove unused UTCTime import

Co-authored-by: andreasabel <[email protected]>

* Fix Makefile TAB characters and simplify sortByModTime

- Restore TAB characters in Makefile (required for make syntax)
- Simplify sortByModTime using Down wrappers and standard tuple ordering
- Remove custom fileOrder function and use standard sort

Co-authored-by: andreasabel <[email protected]>

* Fix Makefile for CI

* Attempt to fix nix CI

* Fix nix CI: add diffutils parameter to agda2hs.nix

The testsuite uses diff, so diffutils needs to be available.
In agda2hs.nix, pkgs refers to the list of Agda packages (not nixpkgs),
so diffutils must be passed as a function parameter via callPackage.

Co-authored-by: andreasabel <[email protected]>

* Disable tests in nix build to fix circular dependency

The testsuite requires the agda2hs binary to be in PATH, but during
nix build of the Haskell package, the binary isn't available yet.
This creates a circular dependency. Use dontCheck to disable tests
in nix builds - tests should be run via `cabal test` in a development
environment instead.

Co-authored-by: andreasabel <[email protected]>

* Address code style review comments

- Restore comments for fixWhitespace, checkWhitespace, have-bin-% targets
- Move .PHONY for have-bin-% to top of file with other .PHONY markers
- Factor out discoverTests function to reduce code duplication
- Use filterM with doesDirectoryExist/doesFileExist in findAgdaFiles
- Refactor relativizeLine to use any (`isInfixOf` rest)
- Use break '/' instead of drop 1 in findTestPrefix

Co-authored-by: andreasabel <[email protected]>

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: andreasabel <[email protected]>
Co-authored-by: Andreas Abel <[email protected]>

Author: Copilot

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,4 +1,5 @@
-.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 have-bin-%
+
 FILES = $(shell find src -type f)
 
 build :
@@ -11,45 +12,57 @@ agda :
 	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
-
 testContainers:
 	cd ./lib/containers && ./generate-haskell.sh && cabal build containers-prop
 
+# Run all tests
 test : checkWhitespace test-on-CI
 
-test-on-CI : test/agda2hs testContainers
-	make -C test
+# Run all tests except for fix-whitespace
+test-on-CI : succeed fail testContainers
+
+# Run only successful tests
+succeed :
+	cabal test agda2hs-test --test-options='-p Succeed'
+
+# Run only failing tests
+fail :
+	cabal test agda2hs-test --test-options='-p Fail'
+
+# 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
 
 FIXW_BIN = fix-whitespace
 
-.PHONY : fixWhitespace ## Fix the whitespace issue.
+## Fix the whitespace issue.
 fixWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
 	$(FIXW_BIN)
 
-.PHONY : checkWhitespace ## Check the whitespace issue without fixing it.
+## Check the whitespace issue without fixing it.
 checkWhitespace : have-bin-$(FIXW_BIN) fix-whitespace.yaml
 	$(FIXW_BIN) --check
 
-.PHONY : have-bin-% ## Installing binaries for developer services
+## Installing binaries for developer services
 have-bin-% :
 	@($* --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:          [email protected]
-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

nix/agda2hs.nix

@@ -12,6 +12,7 @@
   makeWrapper,
   writeText,
   ghcWithPackages,
+  diffutils,
 }:
 
 let
@@ -51,7 +52,10 @@ let
     runCommand "${pname}-${version}"
       {
         inherit pname version;
-        nativeBuildInputs = [ makeWrapper ];
+        nativeBuildInputs = [
+          diffutils
+          makeWrapper
+        ];
         passthru = {
           unwrapped = agda2hs;
           inherit withPackages;

nix/lib.nix

@@ -10,7 +10,10 @@ let
       src = ../.;
       extraCabal2nixOptions = options; # "--jailbreak"
     };
-  hpkg = pkgs.haskellPackages.callPackage (hsrc "") { };
+  # Disable tests in nix build - the testsuite requires the agda2hs binary
+  # to be in PATH, which is a circular dependency. Tests should be run
+  # via `cabal test` in a development environment instead.
+  hpkg = pkgs.haskell.lib.dontCheck (pkgs.haskellPackages.callPackage (hsrc "") { });
   expr = import ./agda2hs.nix;
   agda2hs = pkgs.lib.makeScope pkgs.newScope (
     self:

nix/shell.nix

@@ -24,5 +24,7 @@ pkgs.haskellPackages.shellFor {
     pkgs.nixfmt-rfc-style
     cabal2nix
     pkgs.haskellPackages.fix-whitespace
+    # The testsuite uses diff, so ensure `diff` is available in the shell/tests
+    pkgs.diffutils
   ];
 }