[ fix ] test runner to use cabal (#2884) (#2896)

* [ fix ] add test runner (#2884)

* [ test ] update bounds

This is probably not going to build (missing bytestring / random
dependencies in the sample cabal file).

* [ fix ] relax directory constraints, fix deprecated use

* [ fix ] bytestring dependency

* [ fix ] random dependency

* [ fix ] test runner for random should ignore outputs

* [ fix ] the extra arguments may have spaces in them

* [ cleanup ]

* CI: remove JOSS build
* Test runner: print test name without buffering
* Script: fix issue leading to nested _build/_build/...

* [ re #2896 ] Restrict clock types

* [ oops ] forgot to fix the re-export

* [ fix ] typo 🤦

* [ fix ] this casing is killing me

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

Author: MatthewDaggitt

.github/workflows/ci-ubuntu.yml

@@ -76,8 +76,7 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=3d04bacca842729f9c0869b9287256321b5f450f" >> "${GITHUB_ENV}";
-              # Andreas, 2025-10-07: 3d04bacca842729f9c0869b9287256321b5f450f is tags/v2.8.0
+            echo "AGDA_COMMIT=tags/v2.8.0" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
@@ -170,8 +169,7 @@ jobs:
 
       - name: Golden testing
         run: |
-          ${{ env.CABAL_V1_INSTALL }} clock
-          make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
+          make testsuite INTERACTIVE='' AGDA_EXEC='agda' GHC_EXEC='ghc'
 
 
 ########################################################################

.gitignore

@@ -27,6 +27,7 @@ GenerateEverything
 Haskell
 html
 log
+logs/
 MAlonzo
 output
 runtests

GNUmakefile

@@ -1,3 +1,4 @@
+GHC_EXEC ?= ghc
 AGDA_EXEC ?= agda
 AGDA_OPTIONS=-Werror
 AGDA_RTS_OPTIONS=+RTS -M4.0G -H3.5G -A128M -RTS
@@ -14,7 +15,7 @@ test: doc/Everything.agda check-whitespace
 	cd doc && $(AGDA) README.agda
 
 testsuite:
-	$(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only)
+	$(MAKE) -C tests test GHC_EXEC="$(GHC_EXEC)" AGDA="$(AGDA)" only=$(only)
 
 fix-whitespace:
 	$(CABAL_EXEC) exec -- fix-whitespace

src/System/Clock.agda

@@ -37,20 +37,13 @@ open import System.Clock.Primitive as Prim
         -- System-wide monotonic time since an arbitrary point in the past
         ; monotonic
         -- System-wide real time since the Epoch
-        ; realTime
+        ; realtime
         -- Amount of execution time of the current process
         ; processCPUTime
         -- Amount of execution time of the current OS thread
         ; threadCPUTime
         -- A raw hardware version of Monotonic ignoring adjustments
         ; monotonicRaw
-        -- Linux-specific clocks
-        -- Similar to Monotonic, includes time spent suspended
-        ; bootTime
-        -- Faster but less precise alternative to Monotonic
-        ; monotonicCoarse
-        -- Faster but less precise alternative to RealTime
-        ; realTimeCoarse
         )
 
 ------------------------------------------------------------------------
@@ -86,9 +79,9 @@ record Timed (A : Set a) : Set a where
 
 time : IO A → IO (Timed A)
 time io = do
-  start ← lift! $ getTime realTime
+  start ← lift! $ getTime realtime
   a     ← io
-  end   ← lift! $ getTime realTime
+  end   ← lift! $ getTime realtime
   pure $ mkTimed a $ diff (lower start) (lower end)
 
 time′ : IO {0ℓ} A → IO Time

src/System/Clock/Primitive.agda

@@ -13,17 +13,39 @@ open import IO.Primitive.Core using (IO)
 open import Foreign.Haskell using (Pair)
 
 data Clock : Set where
-  monotonic realTime processCPUTime : Clock
-  threadCPUTime monotonicRaw bootTime : Clock
-  monotonicCoarse realTimeCoarse : Clock
+  monotonic realtime processCPUTime : Clock
+  threadCPUTime monotonicRaw : Clock
 
-{-# COMPILE GHC Clock = data Clock (Monotonic | Realtime | ProcessCPUTime
-                                   | ThreadCPUTime | MonotonicRaw | Boottime
-                                   | MonotonicCoarse | RealtimeCoarse )
+{-# FOREIGN GHC import System.Clock  #-}
+
+{-# FOREIGN GHC
+data AgdaClock
+  = AgdaMonotonic
+  | AgdaRealtime
+  | AgdaProcessCPUTime
+  | AgdaThreadCPUTime
+  | AgdaMonotonicRaw
+
+fromAgdaClock :: AgdaClock -> Clock
+fromAgdaClock ac = case ac of
+  AgdaMonotonic -> Monotonic
+  AgdaRealtime -> Realtime
+  AgdaProcessCPUTime -> ProcessCPUTime
+  AgdaThreadCPUTime -> ThreadCPUTime
+  AgdaMonotonicRaw -> MonotonicRaw
+#-}
+
+{-# COMPILE GHC Clock =
+  data AgdaClock
+  ( AgdaMonotonic
+  | AgdaRealtime
+  | AgdaProcessCPUTime
+  | AgdaThreadCPUTime
+  | AgdaMonotonicRaw
+  )
 #-}
 
 postulate getTime : Clock → IO (Pair Nat Nat)
 
-{-# FOREIGN GHC import System.Clock  #-}
 {-# FOREIGN GHC import Data.Function #-}
-{-# COMPILE GHC getTime = fmap (\ (TimeSpec a b) -> ((,) `on` fromIntegral) a b) . getTime #-}
+{-# COMPILE GHC getTime = fmap (\ (TimeSpec a b) -> ((,) `on` fromIntegral) a b) . getTime . fromAgdaClock #-}

src/Test/Golden.agda

@@ -102,6 +102,7 @@ open import Relation.Nullary.Decidable.Core using (does)
 
 open import Codata.Musical.Notation using (♯_)
 open import IO
+open import IO.Handle
 
 open import System.Clock as Clock using (time′; Time; seconds)
 open import System.Console.ANSI
@@ -205,9 +206,10 @@ runTest opts testPath = do
   true ← doesDirectoryExist (mkFilePath testPath)
     where false → fail directoryNotFound
 
+  putStr $ concat (testPath ∷ ": " ∷ [])
   time ← time′ $ callCommand $ unwords
            $ "cd" ∷ testPath
-           ∷ "&&" ∷ "sh ./run" ∷ opts .exeUnderTest
+           ∷ "&&" ∷ "sh ./run" ∷ (concat $ "\"" ∷ opts .exeUnderTest ∷ "\"" ∷ [])
            ∷ "| tr -d '\\r' > output"
            ∷ []
 
@@ -304,14 +306,14 @@ runTest opts testPath = do
       when b $ writeFile (testPath String.++ "/expected") out
 
     printTiming : Bool → Time → String → IO _
-    printTiming false _    msg = putStrLn $ concat (testPath ∷ ": " ∷ msg ∷ [])
+    printTiming false _    msg = putStrLn msg
     printTiming true  time msg =
       let time  = ℕ.show (time .seconds) String.++ "s"
           spent = 9 + sum (List.map String.length (testPath ∷ time ∷ []))
                -- ^ hack: both "success" and "FAILURE" have the same length
                --   can't use `String.length msg` because the msg contains escape codes
           pad   = String.replicate (72 ∸ spent) ' '
-      in putStrLn (concat (testPath ∷ ": " ∷ msg ∷ pad ∷ time ∷ []))
+      in putStrLn (concat (msg ∷ pad ∷ time ∷ []))
 
 -- A test pool is characterised by
 --  + a name
@@ -385,6 +387,7 @@ poolRunner opts pool = do
 
 runner : List TestPool → IO ⊤
 runner tests = do
+  hSetBuffering stdout noBuffering
   -- figure out the options
   args ← getArgs
   inj₂ opts ← options args

tests/Makefile

@@ -1,13 +1,22 @@
-INTERACTIVE ?= --interactive
+INTERACTIVE   ?= --interactive
+GHC_EXEC      ?= ghc
+CABAL         ?= cabal
+CABAL_OPTIONS ?= --with-compiler $(GHC_EXEC)
 
-runtests: runtests.agda
-	rm -f _build/runtests
-	rm -f _build/MAlonzo/Code/Qruntests*
-	$(AGDA) --compile-dir=_build/ -c runtests.agda
+AGDA_BUILD_DIR  = _config/_build
+CABAL_BUILD_DIR = _config/dist-newstyle
 
-test: runtests
-	./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only)
+./runtests: admin/runtests/Main.agda
+	cd admin/runtests && AGDA="$(AGDA)" sh run
 
+test: ./runtests
+	./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only $(only)
 
-retest: runtests
-	./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only)
+
+retest: ./runtests
+	./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only)
+
+clean:
+	rm -rf runtests
+	rm -rf _config/_build
+	rm -rf _config/dist-newstyle

tests/README.md

@@ -1,32 +1,56 @@
-Test suite
-==========
+# Running the test suite
 
-Building the library
-####################
+You can run the test suite by going back to the main project directory
+and running (change accordingly if you have the right versions of Agda
+& GHC installed but the executable names are different).
 
-You can test the building of the entire library by running the following command from the top-level directory of the library:
-```bash
-cabal run GenerateEverything -- --include-deprecated
-agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc -WnoUserWarning Everything.agda
+```shell
+AGDA_EXEC=agda-2.6.8 GHC_EXEC=ghc-9.12.2 make testsuite
 ```
 
-Golden tests
-############
+# Structure of the test suite
 
-Setup
------
+## Test case
 
-The golden tests need the `clock` package from Cabal to run.
-This can be installed via:
-```bash
-cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' clock
-```
+Each test case is under 2 levels of nesting (this is hard-coded)
+and should comprise:
 
-Running
--------
+1. A `Main.agda` file containing a `main` entrypoint
+2. An `expected` file containing the expected output of running `Main`
+3. A `run` file describing how to run `Main` (most likely implemented
+   using the `goldenTest` function defined in
+   [_config/config.sh](_config/config.sh).
+4. Optionally, an `input` file for the stdin content to feed to
+   the executable obtained by compiling `Main`.
 
-The golden tests can be run from the top-level directory of the library with the command:
-```bash
-make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
-```
-This should take about 5 minutes to run.
+## Configuration
+
+The Agda & GHC version numbers the stdlib is tested against
+are specified in [_config/version-numbers.sh](_config/version-numbers.sh)
+
+## Test runner
+
+The test runner is defined in [admin/runtests/](admin/runtests/).
+It is compiled using an ad-hoc [run](admin/runtests/run) file using
+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
+the [runtests](admin/runtests/Main.agda) program.
+
+## Test dependencies
+
+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 GHC compiler we build against.
+
+# Updating the test suite
+
+1. Update [_config/version-numbers.sh](_config/version-numbers.sh)
+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)
+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

@@ -0,0 +1,90 @@
+#!/bin/sh
+
+# This script is intended to be sourced from test scripts.
+#
+# It provides a number of default config options corresponding
+# to the compiler versions the stdlib is being tested with
+#
+# Usage: . ../../config.sh
+
+set -eu
+
+# Ugh, paths are relative to the script sourcing this file!
+. ../../_config/version-numbers.sh
+
+
+
+# Main entry point to build and run an Agda program
+#
+# Typically called like `goldenTest "$1" "echo" "hello world"`
+#
+# INPUTS:
+#    $1 is the agda executable (typically "$1" in the ̀ run` file
+#       because this info is provided by the test runner
+#    $2 the name of the test as a string
+#    $3 is OPTIONAL and corresponds to the extra arguments to pass
+#       to the executable obtained by compiling the Agda program
+#
+# LOGGING:
+#    logs/agda-build for the trace produced by Agda
+#    logs/cabal-build for the trace produced by cabal+ghc
+#
+# OUTPUT:
+#    the output obtained by running the Agda program is stored in
+#    the file named `output`. The test runner will then diff it
+#    against the expected file.
+goldenTest () {
+
+  AGDA="$1"
+  TEST_NAME="stdlib-test-$2"
+
+  # Taking extra args for the executable?
+  if [ -z "${3-}" ]; then
+    EXTRA_ARGS=""
+  else
+    EXTRA_ARGS="-- $3"
+  fi
+
+  # Remember whether the script has an input -- ugh
+  if [ -f input ]; then
+    HAS_INPUT="true"
+  else
+    touch input
+    HAS_INPUT="false"
+  fi
+
+  # 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
+
+  rm -f _build
+  mkdir -p "$AGDA_BUILD_DIR"
+  ln -sf "$AGDA_BUILD_DIR" .
+  rm -f dist-newstyle
+  mkdir -p "$CABAL_BUILD_DIR"
+  ln -sf "$CABAL_BUILD_DIR" .
+
+  # 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
+  cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build
+
+  # Run the test
+  cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" $EXTRA_ARGS < input > output
+
+  # Clean up after ourselves
+  if ! "$HAS_INPUT"; then
+    rm input
+  fi
+  rm "$TEST_NAME".cabal
+  rm "$TEST_NAME".agda-lib
+  rm _build
+  rm dist-newstyle
+}

tests/_config/libraries

@@ -0,0 +1 @@
+../../../standard-library.agda-lib