[ misc ] various fixes & using a unique cabal file

Author: gallais

src/Test/Golden.agda

@@ -207,7 +207,7 @@ runTest opts testPath = do
   putStr $ concat (testPath ∷ ": " ∷ [])
   time ← time′ $ callCommand $ unwords
            $ "cd" ∷ testPath
-           ∷ "&&" ∷ "sh ./run" ∷ opts .exeUnderTest
+           ∷ "&&" ∷ "sh ./run" ∷ (concat $ "\"" ∷ opts .exeUnderTest ∷ "\"" ∷ [])
            ∷ "| tr -d '\\r' > output"
            ∷ []
 

tests/Makefile

@@ -6,7 +6,7 @@ CABAL_OPTIONS ?= --with-compiler $(GHC_EXEC)
 AGDA_BUILD_DIR  = _config/_build
 CABAL_BUILD_DIR = _config/dist-newstyle
 
-./runtests: admin/runtests/runtests.agda
+./runtests: admin/runtests/Main.agda
 	cd admin/runtests && AGDA="$(AGDA)" sh run
 
 test: ./runtests

tests/README.md

@@ -8,7 +8,6 @@ and running (change accordingly if you have the right versions of Agda
 AGDA_EXEC=agda-2.6.4 GHC_EXEC=ghc-9.2.8 make testsuite
 ```
 
-
 # Structure of the test suite
 
 ## Configuration
@@ -24,24 +23,21 @@ the shared configuration and the resulting executable is copied to
 the root of the tests directory.
 
 If you want to add new tests, you need to list them in
-[runtests.agda](admin/runtests/runtests.agda).
+the [runtests](admin/runtests/Main.agda) program.
 
 ## Test dependencies
 
-The external dependencies of each test are spelt out in:
-
-* either the generic [_config/template.cabal](_config/template.cabal) cabal file
-if they don't need any additional dependencies
-* or the test-specific cabal file (e.g. [data/appending/appending.cabal](data/appending/appending.cabal)) otherwise
+The external dependencies of the whole test suite are spelt out in the generic
+[_config/template.cabal](_config/template.cabal) cabal file
 
 You may need to bump these dependencies when changing
-the version of the compiler backend we build against.
+the version of the GHC compiler we build against.
 
 # Updating the test suite
 
 1. Update [_config/version-numbers.sh](_config/version-numbers.sh)
-2. Update the command listing explicit version numbers at the top of this README
+2. Update the shell command listing explicit version numbers in the
+   fenced code block at the top of this README
 3. Update bounds in [_config/template.cabal](_config/template.cabal)
-   as well as all the test-specific cabal files in the X/Y/ subdirectories
 4. Update [../.github/workflows/ci-ubuntu.yml](../.github/workflows/ci-ubuntu.yml)
    to run the continuous integration with the new GHC and/or Agda versions.

tests/_config/config.sh

@@ -43,7 +43,7 @@ goldenTest () {
   ln -sf "$CABAL_BUILD_DIR" dist-newstyle
 
   # Compile the Agda module and build the generated code
-  $AGDA --library-file=../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
+  "$AGDA" --library-file=../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
   cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build
 
   # Run the test

tests/_config/template.cabal

@@ -1,6 +1,6 @@
 cabal-version:   2.4
 name:            TEST_NAME
-version:         2.0
+version:         0.0
 build-type:      Simple
 description:     Run this test
 license:         MIT
@@ -15,6 +15,11 @@ common common-build-parameters
 
   build-depends:
       base      >= 4.12 && < 4.20
+    , clock     >= 0.8 && <0.9
+    , directory >= 1.3.6 && < 1.3.7
+    , filemanip >= 0.3.6 && < 0.4
+    , filepath  >= 1.4 && <1.6
+    , process   >= 1.6 && <1.7
     , text      >= 2.0 && <2.2
 
   ghc-options: -Wno-missing-home-modules

tests/admin/runtests/Main.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --guardedness #-}
 
-module runtests where
+module Main where
 
 open import Data.List.Base as List using (_∷_; [])
 open import Data.String.Base using (String; _++_)

tests/admin/runtests/run

@@ -5,6 +5,7 @@ TEST_NAME=runtests
 
 # Specialise template agda-lib
 sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib
+sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal
 
 # Set up clean logs directory
 rm -rf logs/
@@ -20,13 +21,14 @@ mkdir -p "$CABAL_BUILD_DIR"
 ln -sf "$CABAL_BUILD_DIR" dist-newstyle
 
 # Compile the Agda module and build the generated code
-$AGDA --library-file ../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc runtests.agda > logs/agda-build
+$AGDA --library-file ../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
 cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build
 
 # Copy the executable to the test root directory
 cp $(find dist-newstyle/ -name "runtests" -type f) ../../
 
 # Clean up after ourselves
 rm "$TEST_NAME".agda-lib
+rm "$TEST_NAME".cabal
 rm _build
 rm dist-newstyle

tests/admin/runtests/runtests.cabal

@@ -1,34 +1,2 @@
-TEST_NAME=environment
-
-# Use the shared version numbers
-. ../../_config/version-numbers.sh
-
-# Specialise template agda-lib & cabal files
-sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib
-sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal
-
-# Set up clean logs directory
-rm -rf logs/
-mkdir logs
-
-# Use shared directories to avoid rechecking stdlib modules
-AGDA_BUILD_DIR=../../_config/_build
-CABAL_BUILD_DIR=../../_config/dist-newstyle
-
-mkdir -p "$AGDA_BUILD_DIR"
-ln -sf "$AGDA_BUILD_DIR" _build
-mkdir -p "$CABAL_BUILD_DIR"
-ln -sf "$CABAL_BUILD_DIR" dist-newstyle
-
-# Compile the Agda module and build the generated code
-$1 --library-file ../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
-cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build
-
-# Run the test
-cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" -- hello world > output
-
-# Clean up after ourselves
-rm "$TEST_NAME".cabal
-rm "$TEST_NAME".agda-lib
-rm _build
-rm dist-newstyle
+. ../../_config/config.sh
+goldenTest $1 "environment"