[ doc ] for various bits

Author: gallais

tests/README.md

@@ -10,6 +10,19 @@ AGDA_EXEC=agda-2.6.4 GHC_EXEC=ghc-9.2.8 make testsuite
 
 # Structure of the test suite
 
+## Test case
+
+Each test case is under 2 levels of nesting (this is hard-coded)
+and should comprise:
+
+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`.
+
 ## Configuration
 
 The Agda & GHC version numbers the stdlib is tested against

tests/_config/config.sh

@@ -7,16 +7,44 @@
 #
 # Usage: . ../../config.sh
 
-set -eu
+set -eux
 
 # 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"
@@ -47,7 +75,7 @@ goldenTest () {
   cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build
 
   # Run the test
-  cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output
+  cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" $EXTRA_ARGS < input > output
 
   # Clean up after ourselves
   if ! "$HAS_INPUT"; then

tests/_config/version-numbers.sh

@@ -7,10 +7,10 @@
 #
 # Usage: . PATH/TO/version-numbers.sh
 
-if [ -z ${AGDA_EXEC} ]; then
+if [ -z ${AGDA_EXEC-} ]; then
     export AGDA_EXEC=agda-2.6.4
 fi
 
-if [ -z ${GHC_EXEC} ]; then
+if [ -z ${GHC_EXEC-} ]; then
   export GHC_EXEC=ghc-9.2.8
 fi

tests/system/environment/expected

@@ -1,3 +1,3 @@
-environment
+stdlib-test-environment
 hello world
 hello back!

tests/system/environment/run

@@ -1,2 +1,2 @@
 . ../../_config/config.sh
-goldenTest "$1" "environment"
+goldenTest "$1" "environment" "hello world"