[ fix ] add test runner (#2884)

.github/workflows/ci-ubuntu.yml

@@ -9,6 +9,7 @@ on:
     branches:
       - master
       - experimental
+      - v2.0-joss-submission
   merge_group:
 
 ########################################################################
@@ -170,8 +171,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/Test/Golden.agda

@@ -205,9 +205,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 +305,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

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.4 GHC_EXEC=ghc-9.2.8 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,88 @@
+#!/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
+
+  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
+  $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

tests/_config/template.agda-lib

@@ -0,0 +1,5 @@
+name: TEST_NAME
+include: .
+depend: standard-library
+flags:
+  --warning=noUnsupportedIndexedMatch

tests/_config/template.cabal

@@ -0,0 +1,31 @@
+cabal-version:   2.4
+name:            TEST_NAME
+version:         0.0
+build-type:      Simple
+description:     Run this test
+license:         MIT
+
+common common-build-parameters
+  default-language:
+    Haskell2010
+
+  default-extensions:
+    PatternGuards
+    PatternSynonyms
+
+  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
+
+executable TEST_NAME
+  import:           common-build-parameters
+  hs-source-dirs:   _build
+  main-is:          MAlonzo/Code/Main.hs
+  ghc-options:      -main-is MAlonzo.Code.Main

tests/_config/version-numbers.sh

@@ -0,0 +1,16 @@
+#!/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: . PATH/TO/version-numbers.sh
+
+if [ -z ${AGDA_EXEC-} ]; then
+    export AGDA_EXEC=agda-2.6.4
+fi
+
+if [ -z ${GHC_EXEC-} ]; then
+  export GHC_EXEC=ghc-9.2.8
+fi

tests/runtests.agda → 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

@@ -0,0 +1,34 @@
+TEST_NAME=runtests
+
+# Use the shared version numbers
+. ../../_config/version-numbers.sh
+
+# 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/
+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
+$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/data/appending/TakeWhile.agda

@@ -13,7 +13,7 @@ import Data.Nat
 open import Relation.Unary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary
-open import Relation.Nullary.Product
+open import Relation.Nullary.Decidable
 
 -- Original bug reported in #1765 by James Wood
 _ : Appending (3 ∷ []) (2 ∷ []) (3 ∷ 2 ∷ [])

tests/data/appending/run

@@ -1,5 +1,2 @@
-$1 --compile-dir=../../_build -c Main.agda > log
-./../../_build/Main < input > output
-
-rm ../../_build/Main
-rm ../../_build/MAlonzo/Code/Main*
+. ../../_config/config.sh
+goldenTest "$1" "appending"