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 <1155218+andreasabel@users.noreply.github.com>

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,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.
@@ -104,7 +104,9 @@ test-suite agda2hs-test
                        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

test/Main.hs

@@ -1,25 +1,24 @@
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-
 module Main where
 
-import Control.Exception (catch, SomeException)
-import Control.Monad (forM, unless)
+import Control.Monad (forM)
 import qualified Data.ByteString.Lazy as LBS
-import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sort, tails)
+import Data.List (isPrefixOf, isSuffixOf, isInfixOf, sortBy)
+import Data.Ord (Down(..), comparing)
 import qualified Data.Text as T
 import qualified Data.Text.Encoding as TE
+import Data.Time.Clock (UTCTime)
 import System.Directory
   ( createDirectoryIfMissing
+  , doesDirectoryExist
   , doesFileExist
   , getCurrentDirectory
+  , getModificationTime
   , getTemporaryDirectory
   , listDirectory
-  , removeFile
   , setCurrentDirectory
   )
 import System.Exit (ExitCode(..))
-import System.FilePath ((</>), dropExtension, makeRelative, takeBaseName, takeDirectory, takeFileName)
+import System.FilePath ((</>), dropExtension, makeRelative, takeDirectory)
 import System.Process (readProcessWithExitCode)
 import Test.Tasty (TestTree, defaultMain, testGroup)
 import Test.Tasty.Golden (goldenVsStringDiff)
@@ -53,23 +52,56 @@ main = do
     ]
 
 -- | Discover all .agda files under the Succeed directory recursively.
+-- Files are ordered by: modification date (newest first), then golden value
+-- modification date (newest first), then alphabetically.
 discoverSucceedTests :: FilePath -> FilePath -> IO [TestTree]
 discoverSucceedTests testDir buildDir = do
   agdaFiles <- findAgdaFilesRecursive (testDir </> "Succeed")
-  forM (sort agdaFiles) $ \agdaFile -> do
+  sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".hs")
+  forM sortedFiles $ \agdaFile -> do
     let testName = dropExtension (makeRelative (testDir </> "Succeed") agdaFile)
         goldenFile = dropExtension agdaFile ++ ".hs"
     return $ succeedTest testDir buildDir testName agdaFile goldenFile
 
 -- | Discover all .agda files under the Fail directory.
+-- Files are ordered by: modification date (newest first), then golden value
+-- modification date (newest first), then alphabetically.
 discoverFailTests :: FilePath -> FilePath -> IO [TestTree]
 discoverFailTests testDir buildDir = do
   agdaFiles <- findAgdaFilesRecursive (testDir </> "Fail")
-  forM (sort agdaFiles) $ \agdaFile -> do
+  sortedFiles <- sortByModTime agdaFiles (\f -> dropExtension f ++ ".err")
+  forM sortedFiles $ \agdaFile -> do
     let testName = dropExtension (makeRelative (testDir </> "Fail") agdaFile)
         goldenFile = dropExtension agdaFile ++ ".err"
     return $ failTest testDir buildDir testName agdaFile goldenFile
 
+-- | Sort files by modification time (newest first), then by golden value
+-- modification time (if it exists), then alphabetically.
+sortByModTime :: [FilePath] -> (FilePath -> FilePath) -> IO [FilePath]
+sortByModTime files goldenPath = do
+  filesWithTimes <- forM files $ \f -> do
+    agdaTime <- getModificationTime f
+    let golden = goldenPath f
+    goldenExists <- doesFileExist golden
+    goldenTime <- if goldenExists
+                    then Just <$> getModificationTime golden
+                    else return Nothing
+    return (f, agdaTime, goldenTime)
+  return $ map (\(f,_,_) -> f) $ sortBy fileOrder filesWithTimes
+  where
+    fileOrder (f1, t1, g1) (f2, t2, g2) =
+      -- First by agda file modification time (newest first)
+      case comparing Down t1 t2 of
+        EQ -> case (g1, g2) of
+          -- Then by golden file modification time (newest first)
+          (Just gt1, Just gt2) -> case comparing Down gt1 gt2 of
+            EQ -> compare f1 f2  -- Finally alphabetically
+            x  -> x
+          (Just _, Nothing) -> LT
+          (Nothing, Just _) -> GT
+          (Nothing, Nothing) -> compare f1 f2
+        x -> x
+
 -- | Find all .agda files recursively in a directory.
 findAgdaFilesRecursive :: FilePath -> IO [FilePath]
 findAgdaFilesRecursive dir = do
@@ -82,17 +114,6 @@ findAgdaFilesRecursive dir = do
       else return [path | ".agda" `isSuffixOf` name]
   return (concat paths)
 
--- | Check if path is a directory.
-doesDirectoryExist :: FilePath -> IO Bool
-doesDirectoryExist path = do
-  exists <- doesFileExist path
-  if exists
-    then return False
-    else do
-      -- If it's not a file, check if it's a directory
-      contents <- listDirectory path `catch` \(_ :: SomeException) -> return []
-      return (not (null contents) || path `elem` ["Succeed", "Fail", "Cubical"])
-
 -- | Create a test for a succeed case.
 -- Runs agda2hs on the .agda file, compares the output .hs to the golden file,
 -- then compiles the .hs file with ghc.
@@ -119,9 +140,6 @@ succeedTest testDir buildDir testName agdaFile goldenFile =
 
     case exitCode of
       ExitSuccess -> do
-        -- Read the generated .hs file from build directory
-        content <- LBS.readFile generatedFile
-
         -- Also run ghc to check the generated code compiles
         -- Add include path for finding imported modules
         (ghcExit, ghcOut, ghcErr) <- readProcessWithExitCode
@@ -130,7 +148,8 @@ succeedTest testDir buildDir testName agdaFile goldenFile =
           ""
 
         case ghcExit of
-          ExitSuccess -> return content
+          -- The generated .hs file is the golden value
+          ExitSuccess -> LBS.readFile generatedFile
           ExitFailure _ -> return $ stringToLBS $
             "GHC compilation failed:\n" ++ ghcOut ++ ghcErr
 
@@ -196,13 +215,6 @@ relativizePaths = unlines . map relativizeLine . lines
       | null s = Nothing
       | otherwise = findTestPrefix (drop 1 s)
 
-    isInfixOf :: String -> String -> Bool
-    isInfixOf needle haystack = any (isPrefixOf needle) (tails haystack)
-
-    tails :: String -> [String]
-    tails [] = [[]]
-    tails s@(_:xs) = s : tails xs
-
 -- | Diff command for golden tests.
 diffCmd :: FilePath -> FilePath -> [String]
 diffCmd ref new = ["diff", "-u", ref, new]