[ cleanup ] Even more sharing!

Author: gallais

tests/Makefile

@@ -3,15 +3,15 @@ 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 --ghc-dont-call-ghc runtests.agda
-	$(CABAL) build $(CABAL_OPTIONS)
+AGDA_BUILD_DIR  = _config/_build
+CABAL_BUILD_DIR = _config/dist-newstyle
 
-test: runtests
-	$(CABAL) exec $(CABAL_OPTIONS) runtests -- $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only)
+./runtests: admin/runtests/runtests.agda
+	cd admin/runtests && sh run
 
+test: ./runtests
+	./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only $(only)
 
-retest: runtests
-	$(CABAL) exec $(CABAL_OPTIONS) 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)

tests/_config/config.sh

@@ -40,7 +40,7 @@ goldenTest () {
   ln -sf "$CABAL_BUILD_DIR" dist-newstyle
 
   # Compile the Agda module and build the generated code
-  $AGDA --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/libraries

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

tests/_config/template.agda-lib

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

tests/admin/runtests/run

@@ -0,0 +1,41 @@
+#!/bin/sh
+
+set -e
+
+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
+
+TEST_NAME=runtests
+
+# Specialise template agda-lib
+sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib
+
+# 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 runtests.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 _build
+rm dist-newstyle

tests/runtests.agda renamed to tests/admin/runtests/runtests.agda

@@ -20,7 +20,7 @@ mkdir -p "$CABAL_BUILD_DIR"
 ln -sf "$CABAL_BUILD_DIR" dist-newstyle
 
 # Compile the Agda module and build the generated code
-$1 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
+$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

tests/runtests.cabal renamed to tests/admin/runtests/runtests.cabal

@@ -21,7 +21,7 @@ mkdir -p "$CABAL_BUILD_DIR"
 ln -sf "$CABAL_BUILD_DIR" dist-newstyle
 
 # Compile the Agda module and build the generated code
-$1 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build
+$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