From 2d24cae56dbfbcf36e10ee401e2cc73c66679b22 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 11:51:36 +0000 Subject: [PATCH 01/31] [ build ] the test runner --- GNUmakefile | 3 ++- tests/Makefile | 12 ++++++++---- tests/runtests.cabal | 34 ++++++++++++++++++++++++++++++++++ 3 files changed, 44 insertions(+), 5 deletions(-) create mode 100644 tests/runtests.cabal diff --git a/GNUmakefile b/GNUmakefile index e744f066cc..60abd97df5 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -1,3 +1,4 @@ +GHC_EXEC ?= ghc AGDA_EXEC ?= agda AGDA_OPTIONS=-Werror AGDA_RTS_OPTIONS=+RTS -M4.0G -H3.5G -A128M -RTS @@ -12,7 +13,7 @@ test: 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)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only) fix-whitespace: cabal exec -- fix-whitespace diff --git a/tests/Makefile b/tests/Makefile index a7b7f57a79..7eacd65820 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,13 +1,17 @@ -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) --compile-dir=_build/ -c --ghc-dont-call-ghc runtests.agda + $(CABAL) build $(CABAL_OPTIONS) test: runtests - ./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only) + $(CABAL) exec $(CABAL_OPTIONS) runtests -- $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only) retest: runtests - ./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only) + $(CABAL) exec $(CABAL_OPTIONS) runtests -- $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only) diff --git a/tests/runtests.cabal b/tests/runtests.cabal new file mode 100644 index 0000000000..ca683eb513 --- /dev/null +++ b/tests/runtests.cabal @@ -0,0 +1,34 @@ +cabal-version: 2.4 +name: runtests +version: 2.0 +build-type: Simple +description: Building the test runner +license: MIT + +tested-with: + GHC == 9.2.8 + +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 runtests + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Qruntests.hs + ghc-options: -main-is MAlonzo.Code.Qruntests From 68f96e5dae5207be262bd451ada3048c90271f8f Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 14:54:26 +0000 Subject: [PATCH 02/31] [ fix ] building the data/appending test Now that this is sorted, the other ones should be easy --- .gitignore | 1 + tests/config.sh | 18 +++++++++++++++ tests/data/appending/appending.agda-lib | 2 ++ tests/data/appending/appending.cabal | 29 +++++++++++++++++++++++++ tests/data/appending/run | 23 ++++++++++++++++---- tests/standard-library-tests.agda-lib | 2 ++ 6 files changed, 71 insertions(+), 4 deletions(-) create mode 100755 tests/config.sh create mode 100644 tests/data/appending/appending.cabal diff --git a/.gitignore b/.gitignore index 1724ffd72e..53ae723cb7 100644 --- a/.gitignore +++ b/.gitignore @@ -27,6 +27,7 @@ GenerateEverything Haskell html log +logs/ MAlonzo output runtests diff --git a/tests/config.sh b/tests/config.sh new file mode 100755 index 0000000000..9803d76be2 --- /dev/null +++ b/tests/config.sh @@ -0,0 +1,18 @@ +#!/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/config.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 diff --git a/tests/data/appending/appending.agda-lib b/tests/data/appending/appending.agda-lib index 3e9fcebbe3..18a43a39dc 100644 --- a/tests/data/appending/appending.agda-lib +++ b/tests/data/appending/appending.agda-lib @@ -1,2 +1,4 @@ name: list include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/appending/appending.cabal b/tests/data/appending/appending.cabal new file mode 100644 index 0000000000..d1a62f3fde --- /dev/null +++ b/tests/data/appending/appending.cabal @@ -0,0 +1,29 @@ +cabal-version: 2.4 +name: appending +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + , text >= 2.0 && <2.2 + + ghc-options: -Wno-missing-home-modules + +executable appending + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/appending/run b/tests/data/appending/run index 77b5071aa7..d1dceab4dc 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,5 +1,20 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main < input > output +# Get configuration information +. ../../config.sh -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build +cabal build appending --with-compiler "$GHC_EXEC" > logs/cabal-build + +# Run the test +cabal exec appending --with-compiler "$GHC_EXEC" < input > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/standard-library-tests.agda-lib b/tests/standard-library-tests.agda-lib index 07abad7e4a..3fa3140283 100644 --- a/tests/standard-library-tests.agda-lib +++ b/tests/standard-library-tests.agda-lib @@ -1,2 +1,4 @@ name: standard-library-tests include: ../src/ . +flags: + --warning=noUnsupportedIndexedMatch \ No newline at end of file From 6e6f3f75b2fac5a67333006d97f3c09d05ba6a3c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 15:09:58 +0000 Subject: [PATCH 03/31] [ fix ] building the data/colist test Some cleanups based on this new use-case --- tests/data/appending/run | 6 ++++-- tests/data/colist/colist.agda-lib | 3 +++ tests/data/colist/colist.cabal | 28 ++++++++++++++++++++++++++++ tests/data/colist/run | 25 +++++++++++++++++++++---- 4 files changed, 56 insertions(+), 6 deletions(-) create mode 100644 tests/data/colist/colist.cabal diff --git a/tests/data/appending/run b/tests/data/appending/run index d1dceab4dc..015435a6d2 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,3 +1,5 @@ +TEST_NAME=appending + # Get configuration information . ../../config.sh @@ -10,10 +12,10 @@ ln -sf ../../_build _build # Compile the Agda module and build the generated code $1 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build -cabal build appending --with-compiler "$GHC_EXEC" > logs/cabal-build +cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build # Run the test -cabal exec appending --with-compiler "$GHC_EXEC" < input > output +cabal exec "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/colist/colist.agda-lib b/tests/data/colist/colist.agda-lib index 93e1607d4d..0108a09e5d 100644 --- a/tests/data/colist/colist.agda-lib +++ b/tests/data/colist/colist.agda-lib @@ -1,2 +1,5 @@ name: colist include: ../../../src/ . + +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/colist/colist.cabal b/tests/data/colist/colist.cabal new file mode 100644 index 0000000000..d314be5b86 --- /dev/null +++ b/tests/data/colist/colist.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: colist +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable colist + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/colist/run b/tests/data/colist/run index f6e7c9b3c0..b3afa7fec3 100644 --- a/tests/data/colist/run +++ b/tests/data/colist/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=colist -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file From 06cc339c4d95e1872b0c31095ce3534ee990d092 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:05:19 +0000 Subject: [PATCH 04/31] [ fix ] another big batch of tests --- tests/data/list/list.agda-lib | 2 ++ tests/data/list/list.cabal | 28 +++++++++++++++++++ tests/data/list/run | 25 ++++++++++++++--- .../rational-unnormalised.agda-lib | 4 ++- .../rational-unnormalised.cabal | 28 +++++++++++++++++++ tests/data/rational-unnormalised/run | 25 ++++++++++++++--- tests/data/rational/rational.agda-lib | 2 ++ tests/data/rational/rational.cabal | 28 +++++++++++++++++++ tests/data/rational/run | 25 ++++++++++++++--- tests/data/trie/run | 25 ++++++++++++++--- tests/data/trie/trie.agda-lib | 2 ++ tests/data/trie/trie.cabal | 28 +++++++++++++++++++ tests/monad/counting/counting.agda-lib | 2 ++ tests/monad/counting/counting.cabal | 28 +++++++++++++++++++ tests/monad/counting/run | 25 ++++++++++++++--- tests/monad/fibonacci/fibonacci.agda-lib | 2 ++ tests/monad/fibonacci/fibonacci.cabal | 28 +++++++++++++++++++ tests/monad/fibonacci/run | 25 ++++++++++++++--- tests/monad/pythagorean/pythagorean.agda-lib | 2 ++ tests/monad/pythagorean/pythagorean.cabal | 28 +++++++++++++++++++ tests/monad/pythagorean/run | 25 ++++++++++++++--- tests/monad/tcm/run | 25 ++++++++++++++--- tests/monad/tcm/tcm.agda-lib | 2 ++ tests/monad/tcm/tcm.cabal | 28 +++++++++++++++++++ .../reflection/assumption/assumption.agda-lib | 2 ++ tests/reflection/assumption/assumption.cabal | 28 +++++++++++++++++++ tests/reflection/assumption/run | 25 ++++++++++++++--- 27 files changed, 460 insertions(+), 37 deletions(-) create mode 100644 tests/data/list/list.cabal create mode 100644 tests/data/rational-unnormalised/rational-unnormalised.cabal create mode 100644 tests/data/rational/rational.cabal create mode 100644 tests/data/trie/trie.cabal create mode 100644 tests/monad/counting/counting.cabal create mode 100644 tests/monad/fibonacci/fibonacci.cabal create mode 100644 tests/monad/pythagorean/pythagorean.cabal create mode 100644 tests/monad/tcm/tcm.cabal create mode 100644 tests/reflection/assumption/assumption.cabal diff --git a/tests/data/list/list.agda-lib b/tests/data/list/list.agda-lib index 3e9fcebbe3..18a43a39dc 100644 --- a/tests/data/list/list.agda-lib +++ b/tests/data/list/list.agda-lib @@ -1,2 +1,4 @@ name: list include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/list/list.cabal b/tests/data/list/list.cabal new file mode 100644 index 0000000000..6b7ce295d6 --- /dev/null +++ b/tests/data/list/list.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: list +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable list + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/list/run b/tests/data/list/run index f6e7c9b3c0..36ebe171e6 100644 --- a/tests/data/list/run +++ b/tests/data/list/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=list -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/data/rational-unnormalised/rational-unnormalised.agda-lib b/tests/data/rational-unnormalised/rational-unnormalised.agda-lib index a42440d4c0..cc1b95a24a 100644 --- a/tests/data/rational-unnormalised/rational-unnormalised.agda-lib +++ b/tests/data/rational-unnormalised/rational-unnormalised.agda-lib @@ -1,2 +1,4 @@ -name: rational +name: rational-unnormalised include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/rational-unnormalised/rational-unnormalised.cabal b/tests/data/rational-unnormalised/rational-unnormalised.cabal new file mode 100644 index 0000000000..e3b7eca2fd --- /dev/null +++ b/tests/data/rational-unnormalised/rational-unnormalised.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: rational-unnormalised +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable rational-unnormalised + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/rational-unnormalised/run b/tests/data/rational-unnormalised/run index f6e7c9b3c0..828147b710 100644 --- a/tests/data/rational-unnormalised/run +++ b/tests/data/rational-unnormalised/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=rational-unnormalised -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/data/rational/rational.agda-lib b/tests/data/rational/rational.agda-lib index a42440d4c0..7c4edd12ac 100644 --- a/tests/data/rational/rational.agda-lib +++ b/tests/data/rational/rational.agda-lib @@ -1,2 +1,4 @@ name: rational include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/rational/rational.cabal b/tests/data/rational/rational.cabal new file mode 100644 index 0000000000..fade52edbd --- /dev/null +++ b/tests/data/rational/rational.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: rational +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable rational + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/rational/run b/tests/data/rational/run index f6e7c9b3c0..74ce0516c3 100644 --- a/tests/data/rational/run +++ b/tests/data/rational/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=rational -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/data/trie/run b/tests/data/trie/run index f6e7c9b3c0..f1411ff415 100644 --- a/tests/data/trie/run +++ b/tests/data/trie/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=trie -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/data/trie/trie.agda-lib b/tests/data/trie/trie.agda-lib index 1e1ae6dec2..ad416871f1 100644 --- a/tests/data/trie/trie.agda-lib +++ b/tests/data/trie/trie.agda-lib @@ -1,2 +1,4 @@ name: trie include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/data/trie/trie.cabal b/tests/data/trie/trie.cabal new file mode 100644 index 0000000000..d9b052e049 --- /dev/null +++ b/tests/data/trie/trie.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: trie +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable trie + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/counting/counting.agda-lib b/tests/monad/counting/counting.agda-lib index 34e6fcee78..d3e7665b23 100644 --- a/tests/monad/counting/counting.agda-lib +++ b/tests/monad/counting/counting.agda-lib @@ -1,2 +1,4 @@ name: counting include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/counting/counting.cabal b/tests/monad/counting/counting.cabal new file mode 100644 index 0000000000..3dc048bd63 --- /dev/null +++ b/tests/monad/counting/counting.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: counting +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable counting + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/counting/run b/tests/monad/counting/run index f6e7c9b3c0..7ed7759c18 100644 --- a/tests/monad/counting/run +++ b/tests/monad/counting/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=counting -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/monad/fibonacci/fibonacci.agda-lib b/tests/monad/fibonacci/fibonacci.agda-lib index 48fa8830d1..54bae11c89 100644 --- a/tests/monad/fibonacci/fibonacci.agda-lib +++ b/tests/monad/fibonacci/fibonacci.agda-lib @@ -1,2 +1,4 @@ name: fibonacci include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/fibonacci/fibonacci.cabal b/tests/monad/fibonacci/fibonacci.cabal new file mode 100644 index 0000000000..9d561ddda0 --- /dev/null +++ b/tests/monad/fibonacci/fibonacci.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: fibonacci +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable fibonacci + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/fibonacci/run b/tests/monad/fibonacci/run index f6e7c9b3c0..da1ab7e4ba 100644 --- a/tests/monad/fibonacci/run +++ b/tests/monad/fibonacci/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=fibonacci -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/monad/pythagorean/pythagorean.agda-lib b/tests/monad/pythagorean/pythagorean.agda-lib index d434562aa8..f3cefdffac 100644 --- a/tests/monad/pythagorean/pythagorean.agda-lib +++ b/tests/monad/pythagorean/pythagorean.agda-lib @@ -1,2 +1,4 @@ name: pythagorean include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/pythagorean/pythagorean.cabal b/tests/monad/pythagorean/pythagorean.cabal new file mode 100644 index 0000000000..a0fee4216b --- /dev/null +++ b/tests/monad/pythagorean/pythagorean.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: pythagorean +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable pythagorean + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/pythagorean/run b/tests/monad/pythagorean/run index f6e7c9b3c0..91b2335f00 100644 --- a/tests/monad/pythagorean/run +++ b/tests/monad/pythagorean/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=pythagorean -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/monad/tcm/run b/tests/monad/tcm/run index f6e7c9b3c0..f86923e3ed 100644 --- a/tests/monad/tcm/run +++ b/tests/monad/tcm/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=tcm -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/monad/tcm/tcm.agda-lib b/tests/monad/tcm/tcm.agda-lib index c7559e3dc4..61ed54ab94 100644 --- a/tests/monad/tcm/tcm.agda-lib +++ b/tests/monad/tcm/tcm.agda-lib @@ -1,2 +1,4 @@ name: tcm include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/tcm/tcm.cabal b/tests/monad/tcm/tcm.cabal new file mode 100644 index 0000000000..5a89cce9ca --- /dev/null +++ b/tests/monad/tcm/tcm.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: tcm +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable tcm + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/reflection/assumption/assumption.agda-lib b/tests/reflection/assumption/assumption.agda-lib index f5d7d392ed..9b30d21e7c 100644 --- a/tests/reflection/assumption/assumption.agda-lib +++ b/tests/reflection/assumption/assumption.agda-lib @@ -1,2 +1,4 @@ name: assumption include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/reflection/assumption/assumption.cabal b/tests/reflection/assumption/assumption.cabal new file mode 100644 index 0000000000..9fe409b395 --- /dev/null +++ b/tests/reflection/assumption/assumption.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: assumption +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable assumption + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/reflection/assumption/run b/tests/reflection/assumption/run index f6e7c9b3c0..6c964ccb20 100644 --- a/tests/reflection/assumption/run +++ b/tests/reflection/assumption/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=assumption -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file From 7c220d32488433da9416c1fc45fb94707d91c28b Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:08:21 +0000 Subject: [PATCH 05/31] [ fix ] cabal exec should not print extra output --- tests/data/appending/run | 2 +- tests/data/colist/run | 2 +- tests/data/list/run | 2 +- tests/data/rational-unnormalised/run | 2 +- tests/data/rational/run | 2 +- tests/data/trie/run | 2 +- tests/monad/counting/run | 2 +- tests/monad/fibonacci/run | 2 +- tests/monad/pythagorean/run | 2 +- tests/monad/tcm/run | 2 +- tests/reflection/assumption/run | 2 +- 11 files changed, 11 insertions(+), 11 deletions(-) diff --git a/tests/data/appending/run b/tests/data/appending/run index 015435a6d2..2c909e1031 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/colist/run b/tests/data/colist/run index b3afa7fec3..ca8baa4f18 100644 --- a/tests/data/colist/run +++ b/tests/data/colist/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/list/run b/tests/data/list/run index 36ebe171e6..8ffa74615a 100644 --- a/tests/data/list/run +++ b/tests/data/list/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/rational-unnormalised/run b/tests/data/rational-unnormalised/run index 828147b710..8f448c33ec 100644 --- a/tests/data/rational-unnormalised/run +++ b/tests/data/rational-unnormalised/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/rational/run b/tests/data/rational/run index 74ce0516c3..5861522e50 100644 --- a/tests/data/rational/run +++ b/tests/data/rational/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/data/trie/run b/tests/data/trie/run index f1411ff415..0a3bfe2eb0 100644 --- a/tests/data/trie/run +++ b/tests/data/trie/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/monad/counting/run b/tests/monad/counting/run index 7ed7759c18..4e390817a8 100644 --- a/tests/monad/counting/run +++ b/tests/monad/counting/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/monad/fibonacci/run b/tests/monad/fibonacci/run index da1ab7e4ba..6e08a1852b 100644 --- a/tests/monad/fibonacci/run +++ b/tests/monad/fibonacci/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/monad/pythagorean/run b/tests/monad/pythagorean/run index 91b2335f00..6dd5fe47bf 100644 --- a/tests/monad/pythagorean/run +++ b/tests/monad/pythagorean/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/monad/tcm/run b/tests/monad/tcm/run index f86923e3ed..aad2ac1b2c 100644 --- a/tests/monad/tcm/run +++ b/tests/monad/tcm/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle diff --git a/tests/reflection/assumption/run b/tests/reflection/assumption/run index 6c964ccb20..d178a56d45 100644 --- a/tests/reflection/assumption/run +++ b/tests/reflection/assumption/run @@ -15,7 +15,7 @@ $1 --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 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves rm -R dist-newstyle From 3fabdc328c43fdc06b10b83c00b415193dc23813 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:21:03 +0000 Subject: [PATCH 06/31] [ done ] with skeletons for all the tests in v2.0 --- tests/show/num/num.agda-lib | 2 ++ tests/show/num/num.cabal | 28 +++++++++++++++++++ tests/show/num/run | 25 ++++++++++++++--- tests/show/reflection/reflection.agda-lib | 2 ++ tests/show/reflection/reflection.cabal | 28 +++++++++++++++++++ tests/show/reflection/run | 25 ++++++++++++++--- tests/show/tree/run | 25 ++++++++++++++--- tests/show/tree/tree.agda-lib | 2 ++ tests/show/tree/tree.cabal | 28 +++++++++++++++++++ tests/system/ansi/ansi.agda-lib | 2 ++ tests/system/ansi/ansi.cabal | 28 +++++++++++++++++++ tests/system/ansi/run | 25 ++++++++++++++--- tests/system/directory/directory.agda-lib | 2 ++ tests/system/directory/directory.cabal | 28 +++++++++++++++++++ tests/system/directory/run | 25 ++++++++++++++--- tests/system/environment/environment.agda-lib | 2 ++ tests/system/environment/environment.cabal | 28 +++++++++++++++++++ tests/system/environment/run | 25 ++++++++++++++--- tests/text/pretty/pretty.agda-lib | 2 ++ tests/text/pretty/pretty.cabal | 28 +++++++++++++++++++ tests/text/pretty/run | 25 ++++++++++++++--- tests/text/printf/printf.agda-lib | 2 ++ tests/text/printf/printf.cabal | 28 +++++++++++++++++++ tests/text/printf/run | 25 ++++++++++++++--- tests/text/regex/regex.agda-lib | 2 ++ tests/text/regex/regex.cabal | 28 +++++++++++++++++++ tests/text/regex/run | 25 ++++++++++++++--- tests/text/tabular/run | 25 ++++++++++++++--- tests/text/tabular/tabular.agda-lib | 2 ++ tests/text/tabular/tabular.cabal | 28 +++++++++++++++++++ 30 files changed, 510 insertions(+), 40 deletions(-) create mode 100644 tests/show/num/num.cabal create mode 100644 tests/show/reflection/reflection.cabal create mode 100644 tests/show/tree/tree.cabal create mode 100644 tests/system/ansi/ansi.cabal create mode 100644 tests/system/directory/directory.cabal create mode 100644 tests/system/environment/environment.cabal create mode 100644 tests/text/pretty/pretty.cabal create mode 100644 tests/text/printf/printf.cabal create mode 100644 tests/text/regex/regex.cabal create mode 100644 tests/text/tabular/tabular.cabal diff --git a/tests/show/num/num.agda-lib b/tests/show/num/num.agda-lib index c1cba66e6f..f11dca8d37 100644 --- a/tests/show/num/num.agda-lib +++ b/tests/show/num/num.agda-lib @@ -1,2 +1,4 @@ name: num include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/show/num/num.cabal b/tests/show/num/num.cabal new file mode 100644 index 0000000000..f40628e52b --- /dev/null +++ b/tests/show/num/num.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: num +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable num + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/show/num/run b/tests/show/num/run index f6e7c9b3c0..5d9df02d7e 100644 --- a/tests/show/num/run +++ b/tests/show/num/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=num -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/show/reflection/reflection.agda-lib b/tests/show/reflection/reflection.agda-lib index 79ffa5c292..124e3a1bee 100644 --- a/tests/show/reflection/reflection.agda-lib +++ b/tests/show/reflection/reflection.agda-lib @@ -1,2 +1,4 @@ name: reflection include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/show/reflection/reflection.cabal b/tests/show/reflection/reflection.cabal new file mode 100644 index 0000000000..23693e7124 --- /dev/null +++ b/tests/show/reflection/reflection.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: reflection +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable reflection + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/show/reflection/run b/tests/show/reflection/run index f6e7c9b3c0..a5f53a149a 100644 --- a/tests/show/reflection/run +++ b/tests/show/reflection/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=reflection -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/show/tree/run b/tests/show/tree/run index f6e7c9b3c0..46eb6c5a4c 100644 --- a/tests/show/tree/run +++ b/tests/show/tree/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=tree -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/show/tree/tree.agda-lib b/tests/show/tree/tree.agda-lib index f659528634..90bc955c60 100644 --- a/tests/show/tree/tree.agda-lib +++ b/tests/show/tree/tree.agda-lib @@ -1,2 +1,4 @@ name: tree include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/show/tree/tree.cabal b/tests/show/tree/tree.cabal new file mode 100644 index 0000000000..d91b9f2f5d --- /dev/null +++ b/tests/show/tree/tree.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: tree +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable tree + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/ansi/ansi.agda-lib b/tests/system/ansi/ansi.agda-lib index 367219e74b..0a7cd153ac 100644 --- a/tests/system/ansi/ansi.agda-lib +++ b/tests/system/ansi/ansi.agda-lib @@ -1,2 +1,4 @@ name: ansi include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/system/ansi/ansi.cabal b/tests/system/ansi/ansi.cabal new file mode 100644 index 0000000000..2a9a7eee90 --- /dev/null +++ b/tests/system/ansi/ansi.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: ansi +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable ansi + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/ansi/run b/tests/system/ansi/run index 20143a4947..42dff8e651 100644 --- a/tests/system/ansi/run +++ b/tests/system/ansi/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main hello world > output +TEST_NAME=ansi -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/system/directory/directory.agda-lib b/tests/system/directory/directory.agda-lib index 6abd1b5e02..f30648533b 100644 --- a/tests/system/directory/directory.agda-lib +++ b/tests/system/directory/directory.agda-lib @@ -1,2 +1,4 @@ name: directory include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/system/directory/directory.cabal b/tests/system/directory/directory.cabal new file mode 100644 index 0000000000..c367ab70b6 --- /dev/null +++ b/tests/system/directory/directory.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: directory +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable directory + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/directory/run b/tests/system/directory/run index f6e7c9b3c0..92101e9ec7 100644 --- a/tests/system/directory/run +++ b/tests/system/directory/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=directory -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/system/environment/environment.agda-lib b/tests/system/environment/environment.agda-lib index bcc0d5b45c..12d0203cf3 100644 --- a/tests/system/environment/environment.agda-lib +++ b/tests/system/environment/environment.agda-lib @@ -1,2 +1,4 @@ name: environment include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/system/environment/environment.cabal b/tests/system/environment/environment.cabal new file mode 100644 index 0000000000..7376440a3b --- /dev/null +++ b/tests/system/environment/environment.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: environment +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable environment + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/environment/run b/tests/system/environment/run index 20143a4947..bb6399de6d 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main hello world > output +TEST_NAME=environment -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/text/pretty/pretty.agda-lib b/tests/text/pretty/pretty.agda-lib index 8ec073abd7..506b773046 100644 --- a/tests/text/pretty/pretty.agda-lib +++ b/tests/text/pretty/pretty.agda-lib @@ -1,2 +1,4 @@ name: pretty include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/text/pretty/pretty.cabal b/tests/text/pretty/pretty.cabal new file mode 100644 index 0000000000..d6dcd60b36 --- /dev/null +++ b/tests/text/pretty/pretty.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: pretty +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable pretty + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/pretty/run b/tests/text/pretty/run index f6e7c9b3c0..52a30dc2be 100644 --- a/tests/text/pretty/run +++ b/tests/text/pretty/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=pretty -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/text/printf/printf.agda-lib b/tests/text/printf/printf.agda-lib index cb42e692e3..73037648f4 100644 --- a/tests/text/printf/printf.agda-lib +++ b/tests/text/printf/printf.agda-lib @@ -1,2 +1,4 @@ name: printf include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/text/printf/printf.cabal b/tests/text/printf/printf.cabal new file mode 100644 index 0000000000..f1dc732582 --- /dev/null +++ b/tests/text/printf/printf.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: printf +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable printf + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/printf/run b/tests/text/printf/run index f6e7c9b3c0..8f7f3d2f16 100644 --- a/tests/text/printf/run +++ b/tests/text/printf/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=printf -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/text/regex/regex.agda-lib b/tests/text/regex/regex.agda-lib index 1c33b14658..e38eefbe4c 100644 --- a/tests/text/regex/regex.agda-lib +++ b/tests/text/regex/regex.agda-lib @@ -1,2 +1,4 @@ name: regex include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/text/regex/regex.cabal b/tests/text/regex/regex.cabal new file mode 100644 index 0000000000..4856a0375f --- /dev/null +++ b/tests/text/regex/regex.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: regex +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable regex + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/regex/run b/tests/text/regex/run index f6e7c9b3c0..d169f96536 100644 --- a/tests/text/regex/run +++ b/tests/text/regex/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=regex -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/text/tabular/run b/tests/text/tabular/run index f6e7c9b3c0..c612ed5944 100644 --- a/tests/text/tabular/run +++ b/tests/text/tabular/run @@ -1,5 +1,22 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output +TEST_NAME=tabular -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +# Get configuration information +. ../../config.sh + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use pre-existing build directory to avoid rechecking stdlib modules +ln -sf ../../_build _build + +# Compile the Agda module and build the generated code +$1 --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" > output + +# Clean up after ourselves +rm -R dist-newstyle +rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/text/tabular/tabular.agda-lib b/tests/text/tabular/tabular.agda-lib index de85f156b1..afc6d9a1da 100644 --- a/tests/text/tabular/tabular.agda-lib +++ b/tests/text/tabular/tabular.agda-lib @@ -1,2 +1,4 @@ name: tabular include: ../../../src/ . +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/text/tabular/tabular.cabal b/tests/text/tabular/tabular.cabal new file mode 100644 index 0000000000..46ec34b9d3 --- /dev/null +++ b/tests/text/tabular/tabular.cabal @@ -0,0 +1,28 @@ +cabal-version: 2.4 +name: tabular +version: 2.0 +build-type: Simple +description: Run this test +license: MIT + +tested-with: + GHC == 9.2.8 + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + + ghc-options: -Wno-missing-home-modules + +executable tabular + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main From 49dc2681e4d3955ad272e660265e2127fedefe83 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:25:22 +0000 Subject: [PATCH 07/31] [ ci ] run revamped testsuite --- .github/workflows/ci-ubuntu.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index a40fe804ad..541bf62c35 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -47,7 +47,7 @@ on: ######################################################################## env: - GHC_VERSION: 8.10.7 + GHC_VERSION: 9.2.8 CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' @@ -169,7 +169,7 @@ jobs: - name: Golden testing run: | ${{ env.CABAL_INSTALL }} clock - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' GHC_EXEC=${{ env.GHC_VERSION }} ######################################################################## From 3cacdde42e7d48b9e9103ba77a62cc6ef262b70f Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:26:07 +0000 Subject: [PATCH 08/31] [ ci ] enable build on v2.0-joss-submission branch --- .github/workflows/ci-ubuntu.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 541bf62c35..909c4cda71 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -8,6 +8,7 @@ on: branches: - master - experimental + - v2.0-joss-submission merge_group: ######################################################################## From e3f483e629b1f2f60f09741f885afdc4164a1b58 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:26:38 +0000 Subject: [PATCH 09/31] [ update ] test case --- tests/system/directory/expected | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/system/directory/expected b/tests/system/directory/expected index f091776e40..93299d2832 100644 --- a/tests/system/directory/expected +++ b/tests/system/directory/expected @@ -1,6 +1,8 @@ Creating tmp1 Creating tmp2 Saw _build +Saw dist-newstyle +Saw logs Saw tmp1 Saw tmp2 Removing tmp1 From 6dff4de9755d86212ff63eb67f9186e64c4aef5b Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:28:39 +0000 Subject: [PATCH 10/31] [ fix ] this test takes extra arguments --- tests/system/environment/run | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/system/environment/run b/tests/system/environment/run index bb6399de6d..eedc4ae7cc 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -15,7 +15,7 @@ $1 --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" > output +cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" -- hello world > output # Clean up after ourselves rm -R dist-newstyle From 171bdcbe909a7c3919e9c1756efad0711dc7f004 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:29:06 +0000 Subject: [PATCH 11/31] [ ci ] bump cache version --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 909c4cda71..01643ba90c 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -99,7 +99,7 @@ jobs: # i.e. if we change either the version of Agda, ghc, or cabal that we want # to use for the build. - name: Cache ~/.cabal directories - uses: actions/cache@v2 + uses: actions/cache@v4 id: cache-cabal with: path: | From 8dbf96c6e57e8a01a577197deac906107cb49005 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:30:22 +0000 Subject: [PATCH 12/31] [ ci ] haskell/actions/setup -> haskell-actions/setup --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 01643ba90c..0df7e59a31 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -114,7 +114,7 @@ jobs: ######################################################################## - name: Install ghc & cabal - uses: haskell/actions/setup@v1 + uses: haskell-actions/setup@v1 with: ghc-version: ${{ env.GHC_VERSION }} cabal-version: ${{ env.CABAL_VERSION }} From 86612f5bf02dd92ec1c399685c9aff6f3728f805 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 16:41:02 +0000 Subject: [PATCH 13/31] [ refactor ] share more code --- tests/_config/config.sh | 18 ++++++++++++++++++ .../num/num.cabal => _config/template.cabal} | 4 ++-- tests/show/num/run | 5 ++++- 3 files changed, 24 insertions(+), 3 deletions(-) create mode 100755 tests/_config/config.sh rename tests/{show/num/num.cabal => _config/template.cabal} (91%) diff --git a/tests/_config/config.sh b/tests/_config/config.sh new file mode 100755 index 0000000000..9803d76be2 --- /dev/null +++ b/tests/_config/config.sh @@ -0,0 +1,18 @@ +#!/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/config.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 diff --git a/tests/show/num/num.cabal b/tests/_config/template.cabal similarity index 91% rename from tests/show/num/num.cabal rename to tests/_config/template.cabal index f40628e52b..e9214acf6d 100644 --- a/tests/show/num/num.cabal +++ b/tests/_config/template.cabal @@ -1,5 +1,5 @@ cabal-version: 2.4 -name: num +name: TEST_NAME version: 2.0 build-type: Simple description: Run this test @@ -21,7 +21,7 @@ common common-build-parameters ghc-options: -Wno-missing-home-modules -executable num +executable TEST_NAME import: common-build-parameters hs-source-dirs: _build main-is: MAlonzo/Code/Main.hs diff --git a/tests/show/num/run b/tests/show/num/run index 5d9df02d7e..c8d35a9497 100644 --- a/tests/show/num/run +++ b/tests/show/num/run @@ -1,7 +1,9 @@ TEST_NAME=num # Get configuration information -. ../../config.sh +. ../../_config/config.sh + +sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal # Set up clean logs directory rm -rf logs/ @@ -18,5 +20,6 @@ cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output # Clean up after ourselves +rm "$TEST_NAME".cabal rm -R dist-newstyle rm -R _build/MAlonzo/Code/ \ No newline at end of file From 4c746a365850ace0b53752b769aa3bee6b0fc8ec Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 17:16:46 +0000 Subject: [PATCH 14/31] [ refactor ] removing a lot of duplicate code --- tests/_config/config.sh | 29 +++++++++++++++++++ .../template.agda-lib} | 2 +- tests/_config/template.cabal | 3 -- tests/data/appending/appending.cabal | 3 -- tests/data/appending/run | 4 ++- tests/data/colist/colist.agda-lib | 5 ---- tests/data/colist/colist.cabal | 28 ------------------ tests/data/colist/run | 24 ++------------- tests/data/list/list.cabal | 28 ------------------ tests/data/list/run | 24 ++------------- .../rational-unnormalised.cabal | 28 ------------------ tests/data/rational-unnormalised/run | 24 ++------------- tests/data/rational/rational.cabal | 28 ------------------ tests/data/rational/run | 24 ++------------- tests/data/trie/run | 24 ++------------- tests/data/trie/trie.cabal | 28 ------------------ tests/monad/counting/counting.cabal | 28 ------------------ tests/monad/counting/run | 24 ++------------- tests/monad/fibonacci/fibonacci.cabal | 28 ------------------ tests/monad/fibonacci/run | 24 ++------------- tests/monad/pythagorean/pythagorean.cabal | 28 ------------------ tests/monad/pythagorean/run | 24 ++------------- tests/monad/tcm/run | 24 ++------------- tests/monad/tcm/tcm.cabal | 28 ------------------ .../reflection/assumption/assumption.agda-lib | 4 --- tests/reflection/assumption/assumption.cabal | 28 ------------------ tests/reflection/assumption/run | 24 ++------------- tests/show/num/num.agda-lib | 4 --- tests/show/num/run | 25 +--------------- tests/show/reflection/reflection.agda-lib | 4 --- tests/show/reflection/reflection.cabal | 28 ------------------ tests/show/reflection/run | 24 ++------------- tests/show/tree/run | 24 ++------------- tests/show/tree/tree.agda-lib | 4 --- tests/show/tree/tree.cabal | 28 ------------------ tests/system/ansi/ansi.cabal | 28 ------------------ tests/system/ansi/run | 24 ++------------- tests/system/directory/directory.cabal | 28 ------------------ tests/system/directory/run | 24 ++------------- tests/system/environment/environment.cabal | 28 ------------------ tests/system/environment/expected | 2 +- tests/system/environment/run | 5 +++- tests/text/pretty/pretty.agda-lib | 4 --- tests/text/pretty/pretty.cabal | 28 ------------------ tests/text/pretty/run | 24 ++------------- tests/text/printf/printf.agda-lib | 4 --- tests/text/printf/printf.cabal | 28 ------------------ tests/text/printf/run | 24 ++------------- tests/text/regex/regex.agda-lib | 4 --- tests/text/regex/regex.cabal | 28 ------------------ tests/text/regex/run | 24 ++------------- tests/text/tabular/run | 24 ++------------- tests/text/tabular/tabular.agda-lib | 4 --- tests/text/tabular/tabular.cabal | 28 ------------------ 54 files changed, 75 insertions(+), 999 deletions(-) rename tests/{data/appending/appending.agda-lib => _config/template.agda-lib} (81%) delete mode 100644 tests/data/colist/colist.agda-lib delete mode 100644 tests/data/colist/colist.cabal delete mode 100644 tests/data/list/list.cabal delete mode 100644 tests/data/rational-unnormalised/rational-unnormalised.cabal delete mode 100644 tests/data/rational/rational.cabal delete mode 100644 tests/data/trie/trie.cabal delete mode 100644 tests/monad/counting/counting.cabal delete mode 100644 tests/monad/fibonacci/fibonacci.cabal delete mode 100644 tests/monad/pythagorean/pythagorean.cabal delete mode 100644 tests/monad/tcm/tcm.cabal delete mode 100644 tests/reflection/assumption/assumption.agda-lib delete mode 100644 tests/reflection/assumption/assumption.cabal delete mode 100644 tests/show/num/num.agda-lib delete mode 100644 tests/show/reflection/reflection.agda-lib delete mode 100644 tests/show/reflection/reflection.cabal delete mode 100644 tests/show/tree/tree.agda-lib delete mode 100644 tests/show/tree/tree.cabal delete mode 100644 tests/system/ansi/ansi.cabal delete mode 100644 tests/system/directory/directory.cabal delete mode 100644 tests/system/environment/environment.cabal delete mode 100644 tests/text/pretty/pretty.agda-lib delete mode 100644 tests/text/pretty/pretty.cabal delete mode 100644 tests/text/printf/printf.agda-lib delete mode 100644 tests/text/printf/printf.cabal delete mode 100644 tests/text/regex/regex.agda-lib delete mode 100644 tests/text/regex/regex.cabal delete mode 100644 tests/text/tabular/tabular.agda-lib delete mode 100644 tests/text/tabular/tabular.cabal diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 9803d76be2..cb1184505f 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -16,3 +16,32 @@ fi if [ -z ${GHC_EXEC} ]; then export GHC_EXEC=ghc-9.2.8 fi + +goldenTest () { + + AGDA=$1 + TEST_NAME=$2 + + 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 pre-existing build directory to avoid rechecking stdlib modules + ln -sf ../../_build _build + + # Compile the Agda module and build the generated code + $AGDA --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" > output + + # Clean up after ourselves + rm "$TEST_NAME".cabal + rm -R dist-newstyle + rm -R _build/MAlonzo/Code/ + +} diff --git a/tests/data/appending/appending.agda-lib b/tests/_config/template.agda-lib similarity index 81% rename from tests/data/appending/appending.agda-lib rename to tests/_config/template.agda-lib index 18a43a39dc..1140035f59 100644 --- a/tests/data/appending/appending.agda-lib +++ b/tests/_config/template.agda-lib @@ -1,4 +1,4 @@ -name: list +name: TEST_NAME include: ../../../src/ . flags: --warning=noUnsupportedIndexedMatch diff --git a/tests/_config/template.cabal b/tests/_config/template.cabal index e9214acf6d..5a422c9ab9 100644 --- a/tests/_config/template.cabal +++ b/tests/_config/template.cabal @@ -5,9 +5,6 @@ build-type: Simple description: Run this test license: MIT -tested-with: - GHC == 9.2.8 - common common-build-parameters default-language: Haskell2010 diff --git a/tests/data/appending/appending.cabal b/tests/data/appending/appending.cabal index d1a62f3fde..f66f711634 100644 --- a/tests/data/appending/appending.cabal +++ b/tests/data/appending/appending.cabal @@ -5,9 +5,6 @@ build-type: Simple description: Run this test license: MIT -tested-with: - GHC == 9.2.8 - common common-build-parameters default-language: Haskell2010 diff --git a/tests/data/appending/run b/tests/data/appending/run index 2c909e1031..12719badb4 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,7 +1,9 @@ TEST_NAME=appending # Get configuration information -. ../../config.sh +. ../../_config/config.sh + +sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib # Set up clean logs directory rm -rf logs/ diff --git a/tests/data/colist/colist.agda-lib b/tests/data/colist/colist.agda-lib deleted file mode 100644 index 0108a09e5d..0000000000 --- a/tests/data/colist/colist.agda-lib +++ /dev/null @@ -1,5 +0,0 @@ -name: colist -include: ../../../src/ . - -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/data/colist/colist.cabal b/tests/data/colist/colist.cabal deleted file mode 100644 index d314be5b86..0000000000 --- a/tests/data/colist/colist.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: colist -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable colist - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/colist/run b/tests/data/colist/run index ca8baa4f18..0fb7178204 100644 --- a/tests/data/colist/run +++ b/tests/data/colist/run @@ -1,22 +1,2 @@ -TEST_NAME=colist - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "colist" diff --git a/tests/data/list/list.cabal b/tests/data/list/list.cabal deleted file mode 100644 index 6b7ce295d6..0000000000 --- a/tests/data/list/list.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: list -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable list - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/list/run b/tests/data/list/run index 8ffa74615a..1ef99f0429 100644 --- a/tests/data/list/run +++ b/tests/data/list/run @@ -1,22 +1,2 @@ -TEST_NAME=list - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "list" diff --git a/tests/data/rational-unnormalised/rational-unnormalised.cabal b/tests/data/rational-unnormalised/rational-unnormalised.cabal deleted file mode 100644 index e3b7eca2fd..0000000000 --- a/tests/data/rational-unnormalised/rational-unnormalised.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: rational-unnormalised -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable rational-unnormalised - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/rational-unnormalised/run b/tests/data/rational-unnormalised/run index 8f448c33ec..d434bbd8cc 100644 --- a/tests/data/rational-unnormalised/run +++ b/tests/data/rational-unnormalised/run @@ -1,22 +1,2 @@ -TEST_NAME=rational-unnormalised - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "rational-unnormalised" diff --git a/tests/data/rational/rational.cabal b/tests/data/rational/rational.cabal deleted file mode 100644 index fade52edbd..0000000000 --- a/tests/data/rational/rational.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: rational -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable rational - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/rational/run b/tests/data/rational/run index 5861522e50..fc6178ef8b 100644 --- a/tests/data/rational/run +++ b/tests/data/rational/run @@ -1,22 +1,2 @@ -TEST_NAME=rational - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "rational" diff --git a/tests/data/trie/run b/tests/data/trie/run index 0a3bfe2eb0..13c459b921 100644 --- a/tests/data/trie/run +++ b/tests/data/trie/run @@ -1,22 +1,2 @@ -TEST_NAME=trie - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "trie" diff --git a/tests/data/trie/trie.cabal b/tests/data/trie/trie.cabal deleted file mode 100644 index d9b052e049..0000000000 --- a/tests/data/trie/trie.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: trie -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable trie - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/counting/counting.cabal b/tests/monad/counting/counting.cabal deleted file mode 100644 index 3dc048bd63..0000000000 --- a/tests/monad/counting/counting.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: counting -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable counting - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/counting/run b/tests/monad/counting/run index 4e390817a8..bb32e62978 100644 --- a/tests/monad/counting/run +++ b/tests/monad/counting/run @@ -1,22 +1,2 @@ -TEST_NAME=counting - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "counting" diff --git a/tests/monad/fibonacci/fibonacci.cabal b/tests/monad/fibonacci/fibonacci.cabal deleted file mode 100644 index 9d561ddda0..0000000000 --- a/tests/monad/fibonacci/fibonacci.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: fibonacci -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable fibonacci - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/fibonacci/run b/tests/monad/fibonacci/run index 6e08a1852b..eebe9b7267 100644 --- a/tests/monad/fibonacci/run +++ b/tests/monad/fibonacci/run @@ -1,22 +1,2 @@ -TEST_NAME=fibonacci - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "fibonacci" diff --git a/tests/monad/pythagorean/pythagorean.cabal b/tests/monad/pythagorean/pythagorean.cabal deleted file mode 100644 index a0fee4216b..0000000000 --- a/tests/monad/pythagorean/pythagorean.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: pythagorean -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable pythagorean - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/monad/pythagorean/run b/tests/monad/pythagorean/run index 6dd5fe47bf..3d18560dfb 100644 --- a/tests/monad/pythagorean/run +++ b/tests/monad/pythagorean/run @@ -1,22 +1,2 @@ -TEST_NAME=pythagorean - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "pythagorean" diff --git a/tests/monad/tcm/run b/tests/monad/tcm/run index aad2ac1b2c..bae7179e41 100644 --- a/tests/monad/tcm/run +++ b/tests/monad/tcm/run @@ -1,22 +1,2 @@ -TEST_NAME=tcm - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "tcm" diff --git a/tests/monad/tcm/tcm.cabal b/tests/monad/tcm/tcm.cabal deleted file mode 100644 index 5a89cce9ca..0000000000 --- a/tests/monad/tcm/tcm.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: tcm -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable tcm - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/reflection/assumption/assumption.agda-lib b/tests/reflection/assumption/assumption.agda-lib deleted file mode 100644 index 9b30d21e7c..0000000000 --- a/tests/reflection/assumption/assumption.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: assumption -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/reflection/assumption/assumption.cabal b/tests/reflection/assumption/assumption.cabal deleted file mode 100644 index 9fe409b395..0000000000 --- a/tests/reflection/assumption/assumption.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: assumption -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable assumption - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/reflection/assumption/run b/tests/reflection/assumption/run index d178a56d45..11a064b5a8 100644 --- a/tests/reflection/assumption/run +++ b/tests/reflection/assumption/run @@ -1,22 +1,2 @@ -TEST_NAME=assumption - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "assumption" diff --git a/tests/show/num/num.agda-lib b/tests/show/num/num.agda-lib deleted file mode 100644 index f11dca8d37..0000000000 --- a/tests/show/num/num.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: num -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/show/num/run b/tests/show/num/run index c8d35a9497..9cb3a0b834 100644 --- a/tests/show/num/run +++ b/tests/show/num/run @@ -1,25 +1,2 @@ -TEST_NAME=num - -# Get configuration information . ../../_config/config.sh - -sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm "$TEST_NAME".cabal -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +goldenTest $1 "num" diff --git a/tests/show/reflection/reflection.agda-lib b/tests/show/reflection/reflection.agda-lib deleted file mode 100644 index 124e3a1bee..0000000000 --- a/tests/show/reflection/reflection.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: reflection -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/show/reflection/reflection.cabal b/tests/show/reflection/reflection.cabal deleted file mode 100644 index 23693e7124..0000000000 --- a/tests/show/reflection/reflection.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: reflection -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable reflection - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/show/reflection/run b/tests/show/reflection/run index a5f53a149a..87148e4047 100644 --- a/tests/show/reflection/run +++ b/tests/show/reflection/run @@ -1,22 +1,2 @@ -TEST_NAME=reflection - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "reflection" diff --git a/tests/show/tree/run b/tests/show/tree/run index 46eb6c5a4c..a7f14094c1 100644 --- a/tests/show/tree/run +++ b/tests/show/tree/run @@ -1,22 +1,2 @@ -TEST_NAME=tree - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "tree" diff --git a/tests/show/tree/tree.agda-lib b/tests/show/tree/tree.agda-lib deleted file mode 100644 index 90bc955c60..0000000000 --- a/tests/show/tree/tree.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: tree -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/show/tree/tree.cabal b/tests/show/tree/tree.cabal deleted file mode 100644 index d91b9f2f5d..0000000000 --- a/tests/show/tree/tree.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: tree -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable tree - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/ansi/ansi.cabal b/tests/system/ansi/ansi.cabal deleted file mode 100644 index 2a9a7eee90..0000000000 --- a/tests/system/ansi/ansi.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: ansi -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable ansi - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/ansi/run b/tests/system/ansi/run index 42dff8e651..6b2916d35d 100644 --- a/tests/system/ansi/run +++ b/tests/system/ansi/run @@ -1,22 +1,2 @@ -TEST_NAME=ansi - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "ansi" diff --git a/tests/system/directory/directory.cabal b/tests/system/directory/directory.cabal deleted file mode 100644 index c367ab70b6..0000000000 --- a/tests/system/directory/directory.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: directory -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable directory - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/directory/run b/tests/system/directory/run index 92101e9ec7..d6b99df9a7 100644 --- a/tests/system/directory/run +++ b/tests/system/directory/run @@ -1,22 +1,2 @@ -TEST_NAME=directory - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "directory" diff --git a/tests/system/environment/environment.cabal b/tests/system/environment/environment.cabal deleted file mode 100644 index 7376440a3b..0000000000 --- a/tests/system/environment/environment.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: environment -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable environment - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/system/environment/expected b/tests/system/environment/expected index 1f387d2af2..f8db7fc15d 100644 --- a/tests/system/environment/expected +++ b/tests/system/environment/expected @@ -1,3 +1,3 @@ -Main +environment hello world hello back! diff --git a/tests/system/environment/run b/tests/system/environment/run index eedc4ae7cc..796b5fe98a 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,7 +1,10 @@ TEST_NAME=environment # Get configuration information -. ../../config.sh +. ../../_config/config.sh + +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/ diff --git a/tests/text/pretty/pretty.agda-lib b/tests/text/pretty/pretty.agda-lib deleted file mode 100644 index 506b773046..0000000000 --- a/tests/text/pretty/pretty.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: pretty -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/text/pretty/pretty.cabal b/tests/text/pretty/pretty.cabal deleted file mode 100644 index d6dcd60b36..0000000000 --- a/tests/text/pretty/pretty.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: pretty -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable pretty - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/pretty/run b/tests/text/pretty/run index 52a30dc2be..3df4e1f5c4 100644 --- a/tests/text/pretty/run +++ b/tests/text/pretty/run @@ -1,22 +1,2 @@ -TEST_NAME=pretty - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "pretty" diff --git a/tests/text/printf/printf.agda-lib b/tests/text/printf/printf.agda-lib deleted file mode 100644 index 73037648f4..0000000000 --- a/tests/text/printf/printf.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: printf -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/text/printf/printf.cabal b/tests/text/printf/printf.cabal deleted file mode 100644 index f1dc732582..0000000000 --- a/tests/text/printf/printf.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: printf -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable printf - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/printf/run b/tests/text/printf/run index 8f7f3d2f16..f36bf5aab5 100644 --- a/tests/text/printf/run +++ b/tests/text/printf/run @@ -1,22 +1,2 @@ -TEST_NAME=printf - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "printf" diff --git a/tests/text/regex/regex.agda-lib b/tests/text/regex/regex.agda-lib deleted file mode 100644 index e38eefbe4c..0000000000 --- a/tests/text/regex/regex.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: regex -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/text/regex/regex.cabal b/tests/text/regex/regex.cabal deleted file mode 100644 index 4856a0375f..0000000000 --- a/tests/text/regex/regex.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: regex -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable regex - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/text/regex/run b/tests/text/regex/run index d169f96536..97993e1557 100644 --- a/tests/text/regex/run +++ b/tests/text/regex/run @@ -1,22 +1,2 @@ -TEST_NAME=regex - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "regex" diff --git a/tests/text/tabular/run b/tests/text/tabular/run index c612ed5944..88f61f42ac 100644 --- a/tests/text/tabular/run +++ b/tests/text/tabular/run @@ -1,22 +1,2 @@ -TEST_NAME=tabular - -# Get configuration information -. ../../config.sh - -# Set up clean logs directory -rm -rf logs/ -mkdir logs - -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build - -# Compile the Agda module and build the generated code -$1 --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" > output - -# Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "tabular" diff --git a/tests/text/tabular/tabular.agda-lib b/tests/text/tabular/tabular.agda-lib deleted file mode 100644 index afc6d9a1da..0000000000 --- a/tests/text/tabular/tabular.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: tabular -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/text/tabular/tabular.cabal b/tests/text/tabular/tabular.cabal deleted file mode 100644 index 46ec34b9d3..0000000000 --- a/tests/text/tabular/tabular.cabal +++ /dev/null @@ -1,28 +0,0 @@ -cabal-version: 2.4 -name: tabular -version: 2.0 -build-type: Simple -description: Run this test -license: MIT - -tested-with: - GHC == 9.2.8 - -common common-build-parameters - default-language: - Haskell2010 - - default-extensions: - PatternGuards - PatternSynonyms - - build-depends: - base >= 4.12 && < 4.20 - - ghc-options: -Wno-missing-home-modules - -executable tabular - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main From 7e48fd029858a67d106c8ad0057dc8fd7dd4a21e Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 17:19:26 +0000 Subject: [PATCH 15/31] [ ci ] fix GHC call --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 0df7e59a31..962ae9dd2e 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -170,7 +170,7 @@ jobs: - name: Golden testing run: | ${{ env.CABAL_INSTALL }} clock - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' GHC_EXEC=${{ env.GHC_VERSION }} + make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' GHC_EXEC=ghc ######################################################################## From b75de2a8f89b4fc45bd3b643644772bf51b37a39 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Wed, 19 Nov 2025 18:03:25 +0000 Subject: [PATCH 16/31] [ fix ] regex test case --- .github/workflows/ci-ubuntu.yml | 2 +- tests/data/list/list.agda-lib | 4 --- .../rational-unnormalised.agda-lib | 4 --- tests/data/rational/rational.agda-lib | 4 --- tests/data/trie/trie.agda-lib | 4 --- tests/monad/counting/counting.agda-lib | 4 --- tests/monad/fibonacci/fibonacci.agda-lib | 4 --- tests/monad/pythagorean/pythagorean.agda-lib | 4 --- tests/monad/tcm/tcm.agda-lib | 4 --- tests/system/ansi/ansi.agda-lib | 4 --- tests/system/directory/directory.agda-lib | 4 --- tests/system/environment/environment.agda-lib | 4 --- tests/text/regex/Main.agda | 29 ++++++++++--------- tests/text/regex/expected | 9 +++--- tests/text/regex/haystack | 4 +++ 15 files changed, 25 insertions(+), 63 deletions(-) delete mode 100644 tests/data/list/list.agda-lib delete mode 100644 tests/data/rational-unnormalised/rational-unnormalised.agda-lib delete mode 100644 tests/data/rational/rational.agda-lib delete mode 100644 tests/data/trie/trie.agda-lib delete mode 100644 tests/monad/counting/counting.agda-lib delete mode 100644 tests/monad/fibonacci/fibonacci.agda-lib delete mode 100644 tests/monad/pythagorean/pythagorean.agda-lib delete mode 100644 tests/monad/tcm/tcm.agda-lib delete mode 100644 tests/system/ansi/ansi.agda-lib delete mode 100644 tests/system/directory/directory.agda-lib delete mode 100644 tests/system/environment/environment.agda-lib create mode 100644 tests/text/regex/haystack diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 962ae9dd2e..f4f8c741a4 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -114,7 +114,7 @@ jobs: ######################################################################## - name: Install ghc & cabal - uses: haskell-actions/setup@v1 + uses: haskell-actions/setup@v2 with: ghc-version: ${{ env.GHC_VERSION }} cabal-version: ${{ env.CABAL_VERSION }} diff --git a/tests/data/list/list.agda-lib b/tests/data/list/list.agda-lib deleted file mode 100644 index 18a43a39dc..0000000000 --- a/tests/data/list/list.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: list -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/data/rational-unnormalised/rational-unnormalised.agda-lib b/tests/data/rational-unnormalised/rational-unnormalised.agda-lib deleted file mode 100644 index cc1b95a24a..0000000000 --- a/tests/data/rational-unnormalised/rational-unnormalised.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: rational-unnormalised -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/data/rational/rational.agda-lib b/tests/data/rational/rational.agda-lib deleted file mode 100644 index 7c4edd12ac..0000000000 --- a/tests/data/rational/rational.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: rational -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/data/trie/trie.agda-lib b/tests/data/trie/trie.agda-lib deleted file mode 100644 index ad416871f1..0000000000 --- a/tests/data/trie/trie.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: trie -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/counting/counting.agda-lib b/tests/monad/counting/counting.agda-lib deleted file mode 100644 index d3e7665b23..0000000000 --- a/tests/monad/counting/counting.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: counting -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/fibonacci/fibonacci.agda-lib b/tests/monad/fibonacci/fibonacci.agda-lib deleted file mode 100644 index 54bae11c89..0000000000 --- a/tests/monad/fibonacci/fibonacci.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: fibonacci -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/pythagorean/pythagorean.agda-lib b/tests/monad/pythagorean/pythagorean.agda-lib deleted file mode 100644 index f3cefdffac..0000000000 --- a/tests/monad/pythagorean/pythagorean.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: pythagorean -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/monad/tcm/tcm.agda-lib b/tests/monad/tcm/tcm.agda-lib deleted file mode 100644 index 61ed54ab94..0000000000 --- a/tests/monad/tcm/tcm.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: tcm -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/system/ansi/ansi.agda-lib b/tests/system/ansi/ansi.agda-lib deleted file mode 100644 index 0a7cd153ac..0000000000 --- a/tests/system/ansi/ansi.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: ansi -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/system/directory/directory.agda-lib b/tests/system/directory/directory.agda-lib deleted file mode 100644 index f30648533b..0000000000 --- a/tests/system/directory/directory.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: directory -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/system/environment/environment.agda-lib b/tests/system/environment/environment.agda-lib deleted file mode 100644 index 12d0203cf3..0000000000 --- a/tests/system/environment/environment.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: environment -include: ../../../src/ . -flags: - --warning=noUnsupportedIndexedMatch diff --git a/tests/text/regex/Main.agda b/tests/text/regex/Main.agda index f1faf04e27..a7c60dba79 100644 --- a/tests/text/regex/Main.agda +++ b/tests/text/regex/Main.agda @@ -24,26 +24,29 @@ show e (yes match) = case toView (toInfix e (match .Match.related)) of λ where ∷ fromList suff ∷ [] -agdaFile : Exp -agdaFile = [ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] + - ∙ singleton '.' - ∙ singleton 'a' - ∙ singleton 'g' - ∙ singleton 'd' - ∙ singleton 'a' - -buildDir : Exp -buildDir = singleton '_' - ∙ ([ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] + ∙ singleton '/') + +hell : Exp +hell = [^ [ ' ' ] ∷ [] ] + + ∙ singleton 'h' + ∙ · ⁇ + ∙ singleton 'e' + ∙ singleton 'l' + ∙ singleton 'l' + ∙ [^ [ ' ' ] ∷ [] ] + + + +her : Exp +her = singleton 'h' + ∙ singleton 'e' + ∙ singleton 'r' regex : Regex regex .Regex.fromStart = false regex .Regex.tillEnd = false regex .Regex.expression - = agdaFile ∣ buildDir + = hell ∣ her main : Main main = run $ do - text ← readFiniteFile "run" + text ← readFiniteFile "haystack" List.forM′ (lines text) $ λ l → putStrLn (show regex $ search (toList l) regex) diff --git a/tests/text/regex/expected b/tests/text/regex/expected index 662485f587..6c2bf2f60e 100644 --- a/tests/text/regex/expected +++ b/tests/text/regex/expected @@ -1,5 +1,4 @@ -Match found: $1 --compile-dir=../../_build -c [Main.agda] > log -Match found: ./../../[_build/]Main > output -No match found -Match found: rm ../../[_build/]Main -Match found: rm ../../[_build/MAlonzo/Code/]Main* +Match found: Se sells sea [shells] by the sea shore +Match found: Oh hello, sorry for the [shpelling] +Match found: She hgas changed [her] bsiness up +Match found: She now sells [her] chisels by the shelter diff --git a/tests/text/regex/haystack b/tests/text/regex/haystack new file mode 100644 index 0000000000..ed20333e38 --- /dev/null +++ b/tests/text/regex/haystack @@ -0,0 +1,4 @@ +Se sells sea shells by the sea shore +Oh hello, sorry for the shpelling +She hgas changed her bsiness up +She now sells her chisels by the shelter \ No newline at end of file From 8149656b25f85b8fb9f437357d1d5ba1aef923e3 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 14:06:58 +0000 Subject: [PATCH 17/31] [ cleanup ] Increase sharing --- tests/_config/config.sh | 17 ++++++++++++----- tests/data/appending/run | 12 ++++++++++-- tests/system/environment/run | 17 +++++++++++++---- 3 files changed, 35 insertions(+), 11 deletions(-) diff --git a/tests/_config/config.sh b/tests/_config/config.sh index cb1184505f..6fc3a8e59e 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -22,6 +22,7 @@ goldenTest () { AGDA=$1 TEST_NAME=$2 + # 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 @@ -29,8 +30,14 @@ goldenTest () { rm -rf logs/ mkdir logs - # Use pre-existing build directory to avoid rechecking stdlib modules - ln -sf ../../_build _build + # 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 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build @@ -41,7 +48,7 @@ goldenTest () { # Clean up after ourselves rm "$TEST_NAME".cabal - rm -R dist-newstyle - rm -R _build/MAlonzo/Code/ - + rm "$TEST_NAME".agda-lib + rm _build + rm dist-newstyle } diff --git a/tests/data/appending/run b/tests/data/appending/run index 12719badb4..cf83a8294f 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -3,14 +3,21 @@ TEST_NAME=appending # Get configuration information . ../../_config/config.sh +# 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 pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build +# 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 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build @@ -20,5 +27,6 @@ cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output # Clean up after ourselves +rm "$TEST_NAME".agda-lib rm -R dist-newstyle rm -R _build/MAlonzo/Code/ \ No newline at end of file diff --git a/tests/system/environment/run b/tests/system/environment/run index 796b5fe98a..8de6f74593 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -3,6 +3,7 @@ TEST_NAME=environment # Get configuration information . ../../_config/config.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 @@ -10,8 +11,14 @@ sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal rm -rf logs/ mkdir logs -# Use pre-existing build directory to avoid rechecking stdlib modules -ln -sf ../../_build _build +# 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 --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build @@ -21,5 +28,7 @@ cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" -- hello world > output # Clean up after ourselves -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +rm "$TEST_NAME".cabal +rm "$TEST_NAME".agda-lib +rm _build +rm dist-newstyle \ No newline at end of file From d2b49a0d60f6c93a8f2514fc85c41b2b05771c32 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 14:12:43 +0000 Subject: [PATCH 18/31] [ cosmetic ] switch it up Making it more interesting than two "her" matches --- tests/text/regex/expected | 2 +- tests/text/regex/haystack | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/text/regex/expected b/tests/text/regex/expected index 6c2bf2f60e..4f24d6402b 100644 --- a/tests/text/regex/expected +++ b/tests/text/regex/expected @@ -1,4 +1,4 @@ Match found: Se sells sea [shells] by the sea shore Match found: Oh hello, sorry for the [shpelling] -Match found: She hgas changed [her] bsiness up +Match found: She hgas changed the bsiness up by moving to [¡hell!] Match found: She now sells [her] chisels by the shelter diff --git a/tests/text/regex/haystack b/tests/text/regex/haystack index ed20333e38..a07ccbd4d6 100644 --- a/tests/text/regex/haystack +++ b/tests/text/regex/haystack @@ -1,4 +1,4 @@ Se sells sea shells by the sea shore Oh hello, sorry for the shpelling -She hgas changed her bsiness up +She hgas changed the bsiness up by moving to ¡hell! She now sells her chisels by the shelter \ No newline at end of file From 89853243677641536fd6c04589bbae89302d3912 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 14:17:03 +0000 Subject: [PATCH 19/31] [ ci ] Don't pre-install clock --- .github/workflows/ci-ubuntu.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index f4f8c741a4..34ccc1ade5 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -169,7 +169,6 @@ jobs: - name: Golden testing run: | - ${{ env.CABAL_INSTALL }} clock make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' GHC_EXEC=ghc From 61714c3ad09d2a6e56ce1d3c8b814dec46a3ed3e Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 15:13:32 +0000 Subject: [PATCH 20/31] [ cleanup ] Even more sharing! --- tests/Makefile | 18 +++++----- tests/_config/config.sh | 2 +- tests/_config/libraries | 1 + tests/_config/template.agda-lib | 3 +- tests/admin/runtests/run | 41 +++++++++++++++++++++++ tests/{ => admin/runtests}/runtests.agda | 0 tests/{ => admin/runtests}/runtests.cabal | 0 tests/data/appending/run | 2 +- tests/standard-library-tests.agda-lib | 4 --- tests/system/environment/run | 2 +- 10 files changed, 56 insertions(+), 17 deletions(-) create mode 100644 tests/_config/libraries create mode 100644 tests/admin/runtests/run rename tests/{ => admin/runtests}/runtests.agda (100%) rename tests/{ => admin/runtests}/runtests.cabal (100%) delete mode 100644 tests/standard-library-tests.agda-lib diff --git a/tests/Makefile b/tests/Makefile index 7eacd65820..9aa0a5bc7d 100644 --- a/tests/Makefile +++ b/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) diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 6fc3a8e59e..780a63f87a 100755 --- a/tests/_config/config.sh +++ b/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 diff --git a/tests/_config/libraries b/tests/_config/libraries new file mode 100644 index 0000000000..ca12fd4ae7 --- /dev/null +++ b/tests/_config/libraries @@ -0,0 +1 @@ +../../../standard-library.agda-lib \ No newline at end of file diff --git a/tests/_config/template.agda-lib b/tests/_config/template.agda-lib index 1140035f59..bd86a0a06c 100644 --- a/tests/_config/template.agda-lib +++ b/tests/_config/template.agda-lib @@ -1,4 +1,5 @@ name: TEST_NAME -include: ../../../src/ . +include: . +depend: standard-library flags: --warning=noUnsupportedIndexedMatch diff --git a/tests/admin/runtests/run b/tests/admin/runtests/run new file mode 100644 index 0000000000..e080db01c9 --- /dev/null +++ b/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 diff --git a/tests/runtests.agda b/tests/admin/runtests/runtests.agda similarity index 100% rename from tests/runtests.agda rename to tests/admin/runtests/runtests.agda diff --git a/tests/runtests.cabal b/tests/admin/runtests/runtests.cabal similarity index 100% rename from tests/runtests.cabal rename to tests/admin/runtests/runtests.cabal diff --git a/tests/data/appending/run b/tests/data/appending/run index cf83a8294f..f6097677e3 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -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 diff --git a/tests/standard-library-tests.agda-lib b/tests/standard-library-tests.agda-lib deleted file mode 100644 index 3fa3140283..0000000000 --- a/tests/standard-library-tests.agda-lib +++ /dev/null @@ -1,4 +0,0 @@ -name: standard-library-tests -include: ../src/ . -flags: - --warning=noUnsupportedIndexedMatch \ No newline at end of file diff --git a/tests/system/environment/run b/tests/system/environment/run index 8de6f74593..0cccb0fbfd 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -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 From 74114fb0fe971fe0b634e404a7b0408f4584b2a6 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 15:45:17 +0000 Subject: [PATCH 21/31] [ doc ] adding a README file --- tests/README.md | 47 +++++++++++++++++++ tests/_config/config.sh | 11 ++--- .../{config.sh => _config/version-numbers.sh} | 4 +- tests/admin/runtests/run | 15 ++---- tests/admin/runtests/runtests.cabal | 3 -- tests/data/appending/run | 4 +- tests/system/environment/run | 4 +- 7 files changed, 58 insertions(+), 30 deletions(-) create mode 100644 tests/README.md rename tests/{config.sh => _config/version-numbers.sh} (89%) mode change 100755 => 100644 diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 0000000000..e51339cebc --- /dev/null +++ b/tests/README.md @@ -0,0 +1,47 @@ +# Running the test suite + +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). + +```shell +AGDA_EXEC=agda-2.6.4 GHC_EXEC=ghc-9.2.8 make testsuite +``` + + +# Structure of the test suite + +## 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 +[runtests.agda](admin/runtests/runtests.agda). + +## 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 + +You may need to bump these dependencies when changing +the version of the compiler backend 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 +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. diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 780a63f87a..7a8c4ffb97 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -5,17 +5,12 @@ # It provides a number of default config options corresponding # to the compiler versions the stdlib is being tested with # -# Usage: . PATH/TO/config.sh +# Usage: . ../../config.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 +# Ugh, paths are relative to the script sourcing this file! +. ../../_config/version-numbers.sh goldenTest () { diff --git a/tests/config.sh b/tests/_config/version-numbers.sh old mode 100755 new mode 100644 similarity index 89% rename from tests/config.sh rename to tests/_config/version-numbers.sh index 9803d76be2..fbfba12f65 --- a/tests/config.sh +++ b/tests/_config/version-numbers.sh @@ -5,9 +5,7 @@ # It provides a number of default config options corresponding # to the compiler versions the stdlib is being tested with # -# Usage: . PATH/TO/config.sh - -set -e +# Usage: . PATH/TO/version-numbers.sh if [ -z ${AGDA_EXEC} ]; then export AGDA_EXEC=agda-2.6.4 diff --git a/tests/admin/runtests/run b/tests/admin/runtests/run index e080db01c9..20b17505d2 100644 --- a/tests/admin/runtests/run +++ b/tests/admin/runtests/run @@ -1,17 +1,8 @@ -#!/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 +# 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 diff --git a/tests/admin/runtests/runtests.cabal b/tests/admin/runtests/runtests.cabal index ca683eb513..99ea9ee62e 100644 --- a/tests/admin/runtests/runtests.cabal +++ b/tests/admin/runtests/runtests.cabal @@ -5,9 +5,6 @@ build-type: Simple description: Building the test runner license: MIT -tested-with: - GHC == 9.2.8 - common common-build-parameters default-language: Haskell2010 diff --git a/tests/data/appending/run b/tests/data/appending/run index f6097677e3..69af6420a4 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,7 +1,7 @@ TEST_NAME=appending -# Get configuration information -. ../../_config/config.sh +# 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 diff --git a/tests/system/environment/run b/tests/system/environment/run index 0cccb0fbfd..d461925f06 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,7 +1,7 @@ TEST_NAME=environment -# Get configuration information -. ../../_config/config.sh +# 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 From 831880686e3f7a8e52c121bc394999db50daa3f3 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 15:52:07 +0000 Subject: [PATCH 22/31] [ ci ] whyyyyy?! --- tests/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/Makefile b/tests/Makefile index 9aa0a5bc7d..545babbee6 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -7,7 +7,7 @@ AGDA_BUILD_DIR = _config/_build CABAL_BUILD_DIR = _config/dist-newstyle ./runtests: admin/runtests/runtests.agda - cd admin/runtests && sh run + cd admin/runtests && AGDA="$(AGDA)" sh run test: ./runtests ./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only $(only) From b5449330620d43488388f2a577127fb9fc90866c Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 16:51:07 +0000 Subject: [PATCH 23/31] [ ci ] grmbl --- .github/workflows/ci-ubuntu.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 34ccc1ade5..750b2e2988 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -169,7 +169,7 @@ jobs: - name: Golden testing run: | - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' GHC_EXEC=ghc + make testsuite INTERACTIVE='' AGDA_EXEC='agda' GHC_EXEC='ghc' ######################################################################## From 3d3726d36baeb029fed12366fe45289398d61b93 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 18:04:08 +0000 Subject: [PATCH 24/31] [ ci ] all the tests require text? --- tests/_config/template.cabal | 1 + tests/data/appending/appending.cabal | 26 --------------------- tests/data/appending/run | 34 ++-------------------------- 3 files changed, 3 insertions(+), 58 deletions(-) delete mode 100644 tests/data/appending/appending.cabal diff --git a/tests/_config/template.cabal b/tests/_config/template.cabal index 5a422c9ab9..3dbfa1a9e0 100644 --- a/tests/_config/template.cabal +++ b/tests/_config/template.cabal @@ -15,6 +15,7 @@ common common-build-parameters build-depends: base >= 4.12 && < 4.20 + , text >= 2.0 && <2.2 ghc-options: -Wno-missing-home-modules diff --git a/tests/data/appending/appending.cabal b/tests/data/appending/appending.cabal deleted file mode 100644 index f66f711634..0000000000 --- a/tests/data/appending/appending.cabal +++ /dev/null @@ -1,26 +0,0 @@ -cabal-version: 2.4 -name: appending -version: 2.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 - , text >= 2.0 && <2.2 - - ghc-options: -Wno-missing-home-modules - -executable appending - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Main.hs - ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/data/appending/run b/tests/data/appending/run index 69af6420a4..854b711019 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,32 +1,2 @@ -TEST_NAME=appending - -# 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 - -# 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" < input > output - -# Clean up after ourselves -rm "$TEST_NAME".agda-lib -rm -R dist-newstyle -rm -R _build/MAlonzo/Code/ \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "appending" From ae839674d424e1c1aeb89ce3951bb20b9c67337d Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 19:51:45 +0000 Subject: [PATCH 25/31] [ fix ] remove useless option --- GNUmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/GNUmakefile b/GNUmakefile index 60abd97df5..85fc330888 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -13,7 +13,7 @@ test: Everything.agda check-whitespace cd doc && $(AGDA) README.agda testsuite: - $(MAKE) -C tests test GHC_EXEC="$(GHC_EXEC)" AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only) + $(MAKE) -C tests test GHC_EXEC="$(GHC_EXEC)" AGDA="$(AGDA)" only=$(only) fix-whitespace: cabal exec -- fix-whitespace From cc608e4b2582f3cc24ce07d0db514b92f432fc52 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 21:16:05 +0000 Subject: [PATCH 26/31] [ fix ] add generic support for input files --- tests/_config/config.sh | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 7a8c4ffb97..e0f47452d6 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -7,7 +7,7 @@ # # Usage: . ../../config.sh -set -e +set -eu # Ugh, paths are relative to the script sourcing this file! . ../../_config/version-numbers.sh @@ -17,6 +17,14 @@ goldenTest () { AGDA=$1 TEST_NAME=$2 + # 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 @@ -39,9 +47,12 @@ goldenTest () { cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build # Run the test - cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" > output + cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" < input > output # Clean up after ourselves + if ! "$HAS_INPUT"; then + rm input + fi rm "$TEST_NAME".cabal rm "$TEST_NAME".agda-lib rm _build From 236fd5f288714cb3c9065c043b4ce5624d1c804e Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 21:53:38 +0000 Subject: [PATCH 27/31] [ test ] eagerly print test name --- src/Test/Golden.agda | 5 +++-- tests/admin/runtests/{runtests.agda => Main.agda} | 0 2 files changed, 3 insertions(+), 2 deletions(-) rename tests/admin/runtests/{runtests.agda => Main.agda} (100%) diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index 43bbd3037e..cd061bb039 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -204,6 +204,7 @@ 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 @@ -303,14 +304,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 + List.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 diff --git a/tests/admin/runtests/runtests.agda b/tests/admin/runtests/Main.agda similarity index 100% rename from tests/admin/runtests/runtests.agda rename to tests/admin/runtests/Main.agda From f8c17d4e2ede112b63ef41334d94325010d441cc Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 22:08:40 +0000 Subject: [PATCH 28/31] [ misc ] various fixes & using a unique cabal file --- src/Test/Golden.agda | 2 +- tests/Makefile | 2 +- tests/README.md | 16 +++++-------- tests/_config/config.sh | 2 +- tests/_config/template.cabal | 7 +++++- tests/admin/runtests/Main.agda | 2 +- tests/admin/runtests/run | 4 +++- tests/admin/runtests/runtests.cabal | 31 ------------------------- tests/system/environment/run | 36 ++--------------------------- 9 files changed, 21 insertions(+), 81 deletions(-) delete mode 100644 tests/admin/runtests/runtests.cabal diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index cd061bb039..e12df07317 100644 --- a/src/Test/Golden.agda +++ b/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" ∷ [] diff --git a/tests/Makefile b/tests/Makefile index 545babbee6..13c137bea1 100644 --- a/tests/Makefile +++ b/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 diff --git a/tests/README.md b/tests/README.md index e51339cebc..ba40b07bae 100644 --- a/tests/README.md +++ b/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. diff --git a/tests/_config/config.sh b/tests/_config/config.sh index e0f47452d6..801a5b95e3 100755 --- a/tests/_config/config.sh +++ b/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 diff --git a/tests/_config/template.cabal b/tests/_config/template.cabal index 3dbfa1a9e0..0fedec34bf 100644 --- a/tests/_config/template.cabal +++ b/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 diff --git a/tests/admin/runtests/Main.agda b/tests/admin/runtests/Main.agda index cf9af60245..16d29516d1 100644 --- a/tests/admin/runtests/Main.agda +++ b/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; _++_) diff --git a/tests/admin/runtests/run b/tests/admin/runtests/run index 20b17505d2..4ecee5c00e 100644 --- a/tests/admin/runtests/run +++ b/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,7 +21,7 @@ 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 @@ -28,5 +29,6 @@ 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 diff --git a/tests/admin/runtests/runtests.cabal b/tests/admin/runtests/runtests.cabal deleted file mode 100644 index 99ea9ee62e..0000000000 --- a/tests/admin/runtests/runtests.cabal +++ /dev/null @@ -1,31 +0,0 @@ -cabal-version: 2.4 -name: runtests -version: 2.0 -build-type: Simple -description: Building the test runner -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 runtests - import: common-build-parameters - hs-source-dirs: _build - main-is: MAlonzo/Code/Qruntests.hs - ghc-options: -main-is MAlonzo.Code.Qruntests diff --git a/tests/system/environment/run b/tests/system/environment/run index d461925f06..07e957e674 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -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 \ No newline at end of file +. ../../_config/config.sh +goldenTest $1 "environment" From 2f9a5a3f8232c4d67a2a382ff82b54ddfba54a84 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Thu, 20 Nov 2025 23:54:34 +0000 Subject: [PATCH 29/31] [ fix ] various escaping things --- tests/Makefile | 5 +++++ tests/_config/config.sh | 4 ++-- tests/data/appending/TakeWhile.agda | 2 +- tests/data/appending/run | 2 +- tests/data/colist/run | 2 +- tests/data/list/run | 2 +- tests/data/rational-unnormalised/run | 2 +- tests/data/rational/run | 2 +- tests/data/trie/run | 2 +- tests/monad/counting/run | 2 +- tests/monad/fibonacci/run | 2 +- tests/monad/pythagorean/run | 2 +- tests/monad/tcm/run | 2 +- tests/reflection/assumption/run | 2 +- tests/show/num/run | 2 +- tests/show/reflection/run | 2 +- tests/show/tree/run | 2 +- tests/system/ansi/run | 2 +- tests/system/directory/run | 2 +- tests/system/environment/run | 2 +- tests/text/pretty/run | 2 +- tests/text/printf/run | 2 +- tests/text/regex/run | 2 +- tests/text/tabular/run | 2 +- 24 files changed, 29 insertions(+), 24 deletions(-) diff --git a/tests/Makefile b/tests/Makefile index 13c137bea1..ee659848e4 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -15,3 +15,8 @@ test: ./runtests 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 diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 801a5b95e3..3375912c7b 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -15,7 +15,7 @@ set -eu goldenTest () { AGDA=$1 - TEST_NAME=$2 + TEST_NAME="stdlib-test-$2" # Remember whether the script has an input -- ugh if [ -f input ]; then @@ -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 diff --git a/tests/data/appending/TakeWhile.agda b/tests/data/appending/TakeWhile.agda index 50f582df27..9cd6acf1e3 100644 --- a/tests/data/appending/TakeWhile.agda +++ b/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 ∷ []) diff --git a/tests/data/appending/run b/tests/data/appending/run index 854b711019..35c7982946 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "appending" +goldenTest "$1" "appending" diff --git a/tests/data/colist/run b/tests/data/colist/run index 0fb7178204..b4dac3d859 100644 --- a/tests/data/colist/run +++ b/tests/data/colist/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "colist" +goldenTest "$1" "colist" diff --git a/tests/data/list/run b/tests/data/list/run index 1ef99f0429..3d4b16ca75 100644 --- a/tests/data/list/run +++ b/tests/data/list/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "list" +goldenTest "$1" "list" diff --git a/tests/data/rational-unnormalised/run b/tests/data/rational-unnormalised/run index d434bbd8cc..0716066e91 100644 --- a/tests/data/rational-unnormalised/run +++ b/tests/data/rational-unnormalised/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "rational-unnormalised" +goldenTest "$1" "rational-unnormalised" diff --git a/tests/data/rational/run b/tests/data/rational/run index fc6178ef8b..b81665946a 100644 --- a/tests/data/rational/run +++ b/tests/data/rational/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "rational" +goldenTest "$1" "rational" diff --git a/tests/data/trie/run b/tests/data/trie/run index 13c459b921..0ac4190b78 100644 --- a/tests/data/trie/run +++ b/tests/data/trie/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "trie" +goldenTest "$1" "trie" diff --git a/tests/monad/counting/run b/tests/monad/counting/run index bb32e62978..24e733e240 100644 --- a/tests/monad/counting/run +++ b/tests/monad/counting/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "counting" +goldenTest "$1" "counting" diff --git a/tests/monad/fibonacci/run b/tests/monad/fibonacci/run index eebe9b7267..4d4b6bf028 100644 --- a/tests/monad/fibonacci/run +++ b/tests/monad/fibonacci/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "fibonacci" +goldenTest "$1" "fibonacci" diff --git a/tests/monad/pythagorean/run b/tests/monad/pythagorean/run index 3d18560dfb..f35fce4c89 100644 --- a/tests/monad/pythagorean/run +++ b/tests/monad/pythagorean/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "pythagorean" +goldenTest "$1" "pythagorean" diff --git a/tests/monad/tcm/run b/tests/monad/tcm/run index bae7179e41..e29253c133 100644 --- a/tests/monad/tcm/run +++ b/tests/monad/tcm/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "tcm" +goldenTest "$1" "tcm" diff --git a/tests/reflection/assumption/run b/tests/reflection/assumption/run index 11a064b5a8..c1050c39b7 100644 --- a/tests/reflection/assumption/run +++ b/tests/reflection/assumption/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "assumption" +goldenTest "$1" "assumption" diff --git a/tests/show/num/run b/tests/show/num/run index 9cb3a0b834..d09825bf26 100644 --- a/tests/show/num/run +++ b/tests/show/num/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "num" +goldenTest "$1" "num" diff --git a/tests/show/reflection/run b/tests/show/reflection/run index 87148e4047..938c2c379a 100644 --- a/tests/show/reflection/run +++ b/tests/show/reflection/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "reflection" +goldenTest "$1" "reflection" diff --git a/tests/show/tree/run b/tests/show/tree/run index a7f14094c1..61fd29c26c 100644 --- a/tests/show/tree/run +++ b/tests/show/tree/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "tree" +goldenTest "$1" "tree" diff --git a/tests/system/ansi/run b/tests/system/ansi/run index 6b2916d35d..2ca1dc4e04 100644 --- a/tests/system/ansi/run +++ b/tests/system/ansi/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "ansi" +goldenTest "$1" "ansi" diff --git a/tests/system/directory/run b/tests/system/directory/run index d6b99df9a7..528b57abde 100644 --- a/tests/system/directory/run +++ b/tests/system/directory/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "directory" +goldenTest "$1" "directory" diff --git a/tests/system/environment/run b/tests/system/environment/run index 07e957e674..d6a27fcaeb 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "environment" +goldenTest "$1" "environment" diff --git a/tests/text/pretty/run b/tests/text/pretty/run index 3df4e1f5c4..fc4d8e6310 100644 --- a/tests/text/pretty/run +++ b/tests/text/pretty/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "pretty" +goldenTest "$1" "pretty" diff --git a/tests/text/printf/run b/tests/text/printf/run index f36bf5aab5..0dd6507ca2 100644 --- a/tests/text/printf/run +++ b/tests/text/printf/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "printf" +goldenTest "$1" "printf" diff --git a/tests/text/regex/run b/tests/text/regex/run index 97993e1557..c19ca4c1d7 100644 --- a/tests/text/regex/run +++ b/tests/text/regex/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "regex" +goldenTest "$1" "regex" diff --git a/tests/text/tabular/run b/tests/text/tabular/run index 88f61f42ac..5a4022629a 100644 --- a/tests/text/tabular/run +++ b/tests/text/tabular/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest $1 "tabular" +goldenTest "$1" "tabular" From b53aa9cbb1917ac23705877b6adf7de6b9ee09ef Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 21 Nov 2025 00:40:43 +0000 Subject: [PATCH 30/31] [ doc ] for various bits --- tests/README.md | 13 +++++++++++++ tests/_config/config.sh | 32 +++++++++++++++++++++++++++++-- tests/_config/version-numbers.sh | 4 ++-- tests/system/environment/expected | 2 +- tests/system/environment/run | 2 +- 5 files changed, 47 insertions(+), 6 deletions(-) diff --git a/tests/README.md b/tests/README.md index ba40b07bae..989c9478fa 100644 --- a/tests/README.md +++ b/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 diff --git a/tests/_config/config.sh b/tests/_config/config.sh index 3375912c7b..aaa729dec0 100755 --- a/tests/_config/config.sh +++ b/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 diff --git a/tests/_config/version-numbers.sh b/tests/_config/version-numbers.sh index fbfba12f65..46436a5d29 100644 --- a/tests/_config/version-numbers.sh +++ b/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 diff --git a/tests/system/environment/expected b/tests/system/environment/expected index f8db7fc15d..5923f67e28 100644 --- a/tests/system/environment/expected +++ b/tests/system/environment/expected @@ -1,3 +1,3 @@ -environment +stdlib-test-environment hello world hello back! diff --git a/tests/system/environment/run b/tests/system/environment/run index d6a27fcaeb..68c4b3ee25 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,2 +1,2 @@ . ../../_config/config.sh -goldenTest "$1" "environment" +goldenTest "$1" "environment" "hello world" From 0749e7dc29fd76dd08dce257551edb0a96b638e3 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 21 Nov 2025 00:46:42 +0000 Subject: [PATCH 31/31] [ admin ] removing debug tracing --- tests/_config/config.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/_config/config.sh b/tests/_config/config.sh index aaa729dec0..4a8a1480b6 100755 --- a/tests/_config/config.sh +++ b/tests/_config/config.sh @@ -7,7 +7,7 @@ # # Usage: . ../../config.sh -set -eux +set -eu # Ugh, paths are relative to the script sourcing this file! . ../../_config/version-numbers.sh