diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 3020af8754..4c40d4e3ea 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -9,6 +9,7 @@ on: branches: - master - experimental + - v2.0-joss-submission merge_group: ######################################################################## @@ -170,8 +171,7 @@ jobs: - name: Golden testing run: | - ${{ env.CABAL_V1_INSTALL }} clock - make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' + make testsuite INTERACTIVE='' AGDA_EXEC='agda' GHC_EXEC='ghc' ######################################################################## 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/GNUmakefile b/GNUmakefile index ea55919270..4744bd5cb7 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 @@ -14,7 +15,7 @@ test: doc/Everything.agda check-whitespace cd doc && $(AGDA) README.agda testsuite: - $(MAKE) -C tests test AGDA="$(AGDA)" AGDA_EXEC="$(AGDA_EXEC)" only=$(only) + $(MAKE) -C tests test GHC_EXEC="$(GHC_EXEC)" AGDA="$(AGDA)" only=$(only) fix-whitespace: $(CABAL_EXEC) exec -- fix-whitespace diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index ecababe7c8..051bec2c68 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -205,9 +205,10 @@ runTest opts testPath = do true ← doesDirectoryExist (mkFilePath testPath) where false → fail directoryNotFound + putStr $ concat (testPath ∷ ": " ∷ []) time ← time′ $ callCommand $ unwords $ "cd" ∷ testPath - ∷ "&&" ∷ "sh ./run" ∷ opts .exeUnderTest + ∷ "&&" ∷ "sh ./run" ∷ (concat $ "\"" ∷ opts .exeUnderTest ∷ "\"" ∷ []) ∷ "| tr -d '\\r' > output" ∷ [] @@ -304,14 +305,14 @@ runTest opts testPath = do when b $ writeFile (testPath String.++ "/expected") out printTiming : Bool → Time → String → IO _ - printTiming false _ msg = putStrLn $ concat (testPath ∷ ": " ∷ msg ∷ []) + printTiming false _ msg = putStrLn msg printTiming true time msg = let time = ℕ.show (time .seconds) String.++ "s" spent = 9 + sum (List.map String.length (testPath ∷ time ∷ [])) -- ^ hack: both "success" and "FAILURE" have the same length -- can't use `String.length msg` because the msg contains escape codes pad = String.replicate (72 ∸ spent) ' ' - in putStrLn (concat (testPath ∷ ": " ∷ msg ∷ pad ∷ time ∷ [])) + in putStrLn (concat (msg ∷ pad ∷ time ∷ [])) -- A test pool is characterised by -- + a name diff --git a/tests/Makefile b/tests/Makefile index a7b7f57a79..ee659848e4 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,13 +1,22 @@ -INTERACTIVE ?= --interactive +INTERACTIVE ?= --interactive +GHC_EXEC ?= ghc +CABAL ?= cabal +CABAL_OPTIONS ?= --with-compiler $(GHC_EXEC) -runtests: runtests.agda - rm -f _build/runtests - rm -f _build/MAlonzo/Code/Qruntests* - $(AGDA) --compile-dir=_build/ -c runtests.agda +AGDA_BUILD_DIR = _config/_build +CABAL_BUILD_DIR = _config/dist-newstyle -test: runtests - ./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only $(only) +./runtests: admin/runtests/Main.agda + cd admin/runtests && AGDA="$(AGDA)" sh run +test: ./runtests + ./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only $(only) -retest: runtests - ./_build/runtests $(AGDA_EXEC) $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only) + +retest: ./runtests + ./runtests "$(AGDA)" $(INTERACTIVE) --timing --failure-file failures --only-file failures --only $(only) + +clean: + rm -rf runtests + rm -rf _config/_build + rm -rf _config/dist-newstyle diff --git a/tests/README.md b/tests/README.md index b931b7c728..989c9478fa 100644 --- a/tests/README.md +++ b/tests/README.md @@ -1,32 +1,56 @@ -Test suite -========== +# Running the test suite -Building the library -#################### +You can run the test suite by going back to the main project directory +and running (change accordingly if you have the right versions of Agda +& GHC installed but the executable names are different). -You can test the building of the entire library by running the following command from the top-level directory of the library: -```bash -cabal run GenerateEverything -- --include-deprecated -agda -Werror +RTS -M5G -H3.5G -A128M -RTS -i. -isrc -idoc -WnoUserWarning Everything.agda +```shell +AGDA_EXEC=agda-2.6.4 GHC_EXEC=ghc-9.2.8 make testsuite ``` -Golden tests -############ +# Structure of the test suite -Setup ------ +## Test case -The golden tests need the `clock` package from Cabal to run. -This can be installed via: -```bash -cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS' clock -``` +Each test case is under 2 levels of nesting (this is hard-coded) +and should comprise: -Running -------- +1. A `Main.agda` file containing a `main` entrypoint +2. An `expected` file containing the expected output of running `Main` +3. A `run` file describing how to run `Main` (most likely implemented + using the `goldenTest` function defined in + [_config/config.sh](_config/config.sh). +4. Optionally, an `input` file for the stdin content to feed to + the executable obtained by compiling `Main`. -The golden tests can be run from the top-level directory of the library with the command: -```bash -make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda' -``` -This should take about 5 minutes to run. +## Configuration + +The Agda & GHC version numbers the stdlib is tested against +are specified in [_config/version-numbers.sh](_config/version-numbers.sh) + +## Test runner + +The test runner is defined in [admin/runtests/](admin/runtests/). +It is compiled using an ad-hoc [run](admin/runtests/run) file using +the shared configuration and the resulting executable is copied to +the root of the tests directory. + +If you want to add new tests, you need to list them in +the [runtests](admin/runtests/Main.agda) program. + +## Test dependencies + +The external dependencies of the whole test suite are spelt out in the generic +[_config/template.cabal](_config/template.cabal) cabal file + +You may need to bump these dependencies when changing +the version of the GHC compiler we build against. + +# Updating the test suite + +1. Update [_config/version-numbers.sh](_config/version-numbers.sh) +2. Update the shell command listing explicit version numbers in the + fenced code block at the top of this README +3. Update bounds in [_config/template.cabal](_config/template.cabal) +4. Update [../.github/workflows/ci-ubuntu.yml](../.github/workflows/ci-ubuntu.yml) + to run the continuous integration with the new GHC and/or Agda versions. diff --git a/tests/_config/config.sh b/tests/_config/config.sh new file mode 100755 index 0000000000..4a8a1480b6 --- /dev/null +++ b/tests/_config/config.sh @@ -0,0 +1,88 @@ +#!/bin/sh + +# This script is intended to be sourced from test scripts. +# +# It provides a number of default config options corresponding +# to the compiler versions the stdlib is being tested with +# +# Usage: . ../../config.sh + +set -eu + +# Ugh, paths are relative to the script sourcing this file! +. ../../_config/version-numbers.sh + + + +# Main entry point to build and run an Agda program +# +# Typically called like `goldenTest "$1" "echo" "hello world"` +# +# INPUTS: +# $1 is the agda executable (typically "$1" in the ̀ run` file +# because this info is provided by the test runner +# $2 the name of the test as a string +# $3 is OPTIONAL and corresponds to the extra arguments to pass +# to the executable obtained by compiling the Agda program +# +# LOGGING: +# logs/agda-build for the trace produced by Agda +# logs/cabal-build for the trace produced by cabal+ghc +# +# OUTPUT: +# the output obtained by running the Agda program is stored in +# the file named `output`. The test runner will then diff it +# against the expected file. +goldenTest () { + + AGDA=$1 + TEST_NAME="stdlib-test-$2" + + # Taking extra args for the executable? + if [ -z ${3-} ]; then + EXTRA_ARGS="" + else + EXTRA_ARGS="-- $3" + fi + + # Remember whether the script has an input -- ugh + if [ -f input ]; then + HAS_INPUT="true" + else + touch input + HAS_INPUT="false" + fi + + # Specialise template agda-lib & cabal files + sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib + sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal + + # Set up clean logs directory + rm -rf logs/ + mkdir logs + + # Use shared directories to avoid rechecking stdlib modules + AGDA_BUILD_DIR=../../_config/_build + CABAL_BUILD_DIR=../../_config/dist-newstyle + + mkdir -p "$AGDA_BUILD_DIR" + ln -sf "$AGDA_BUILD_DIR" _build + mkdir -p "$CABAL_BUILD_DIR" + ln -sf "$CABAL_BUILD_DIR" dist-newstyle + + # Compile the Agda module and build the generated code + $AGDA --library-file=../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build + cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build + + # Run the test + cabal exec -v0 "$TEST_NAME" --with-compiler "$GHC_EXEC" $EXTRA_ARGS < input > output + + # Clean up after ourselves + if ! "$HAS_INPUT"; then + rm input + fi + rm "$TEST_NAME".cabal + rm "$TEST_NAME".agda-lib + rm _build + rm dist-newstyle +} 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 new file mode 100644 index 0000000000..bd86a0a06c --- /dev/null +++ b/tests/_config/template.agda-lib @@ -0,0 +1,5 @@ +name: TEST_NAME +include: . +depend: standard-library +flags: + --warning=noUnsupportedIndexedMatch diff --git a/tests/_config/template.cabal b/tests/_config/template.cabal new file mode 100644 index 0000000000..0fedec34bf --- /dev/null +++ b/tests/_config/template.cabal @@ -0,0 +1,31 @@ +cabal-version: 2.4 +name: TEST_NAME +version: 0.0 +build-type: Simple +description: Run this test +license: MIT + +common common-build-parameters + default-language: + Haskell2010 + + default-extensions: + PatternGuards + PatternSynonyms + + build-depends: + base >= 4.12 && < 4.20 + , clock >= 0.8 && <0.9 + , directory >= 1.3.6 && < 1.3.7 + , filemanip >= 0.3.6 && < 0.4 + , filepath >= 1.4 && <1.6 + , process >= 1.6 && <1.7 + , text >= 2.0 && <2.2 + + ghc-options: -Wno-missing-home-modules + +executable TEST_NAME + import: common-build-parameters + hs-source-dirs: _build + main-is: MAlonzo/Code/Main.hs + ghc-options: -main-is MAlonzo.Code.Main diff --git a/tests/_config/version-numbers.sh b/tests/_config/version-numbers.sh new file mode 100644 index 0000000000..46436a5d29 --- /dev/null +++ b/tests/_config/version-numbers.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +# This script is intended to be sourced from test scripts. +# +# It provides a number of default config options corresponding +# to the compiler versions the stdlib is being tested with +# +# Usage: . PATH/TO/version-numbers.sh + +if [ -z ${AGDA_EXEC-} ]; then + export AGDA_EXEC=agda-2.6.4 +fi + +if [ -z ${GHC_EXEC-} ]; then + export GHC_EXEC=ghc-9.2.8 +fi diff --git a/tests/runtests.agda b/tests/admin/runtests/Main.agda similarity index 98% rename from tests/runtests.agda rename to tests/admin/runtests/Main.agda index dcfc3a1256..5551b202ae 100644 --- a/tests/runtests.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 new file mode 100644 index 0000000000..4ecee5c00e --- /dev/null +++ b/tests/admin/runtests/run @@ -0,0 +1,34 @@ +TEST_NAME=runtests + +# Use the shared version numbers +. ../../_config/version-numbers.sh + +# Specialise template agda-lib +sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.agda-lib > "$TEST_NAME".agda-lib +sed "s/TEST_NAME/$TEST_NAME/g" ../../_config/template.cabal > "$TEST_NAME".cabal + +# Set up clean logs directory +rm -rf logs/ +mkdir logs + +# Use shared directories to avoid rechecking stdlib modules +AGDA_BUILD_DIR=../../_config/_build +CABAL_BUILD_DIR=../../_config/dist-newstyle + +mkdir -p "$AGDA_BUILD_DIR" +ln -sf "$AGDA_BUILD_DIR" _build +mkdir -p "$CABAL_BUILD_DIR" +ln -sf "$CABAL_BUILD_DIR" dist-newstyle + +# Compile the Agda module and build the generated code +$AGDA --library-file ../../_config/libraries --compile-dir=_build -c --ghc-dont-call-ghc Main.agda > logs/agda-build +cabal build "$TEST_NAME" --with-compiler "$GHC_EXEC" > logs/cabal-build + +# Copy the executable to the test root directory +cp $(find dist-newstyle/ -name "runtests" -type f) ../../ + +# Clean up after ourselves +rm "$TEST_NAME".agda-lib +rm "$TEST_NAME".cabal +rm _build +rm dist-newstyle 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/appending.agda-lib b/tests/data/appending/appending.agda-lib deleted file mode 100644 index 3e9fcebbe3..0000000000 --- a/tests/data/appending/appending.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: list -include: ../../../src/ . diff --git a/tests/data/appending/run b/tests/data/appending/run index 77b5071aa7..35c7982946 100644 --- a/tests/data/appending/run +++ b/tests/data/appending/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main < input > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "appending" diff --git a/tests/data/colist/colist.agda-lib b/tests/data/colist/colist.agda-lib deleted file mode 100644 index 93e1607d4d..0000000000 --- a/tests/data/colist/colist.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: colist -include: ../../../src/ . diff --git a/tests/data/colist/run b/tests/data/colist/run index f6e7c9b3c0..b4dac3d859 100644 --- a/tests/data/colist/run +++ b/tests/data/colist/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "colist" diff --git a/tests/data/list/list.agda-lib b/tests/data/list/list.agda-lib deleted file mode 100644 index 3e9fcebbe3..0000000000 --- a/tests/data/list/list.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: list -include: ../../../src/ . diff --git a/tests/data/list/run b/tests/data/list/run index f6e7c9b3c0..3d4b16ca75 100644 --- a/tests/data/list/run +++ b/tests/data/list/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "list" 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 a42440d4c0..0000000000 --- a/tests/data/rational-unnormalised/rational-unnormalised.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: rational -include: ../../../src/ . diff --git a/tests/data/rational-unnormalised/run b/tests/data/rational-unnormalised/run index f6e7c9b3c0..0716066e91 100644 --- a/tests/data/rational-unnormalised/run +++ b/tests/data/rational-unnormalised/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "rational-unnormalised" diff --git a/tests/data/rational/rational.agda-lib b/tests/data/rational/rational.agda-lib deleted file mode 100644 index a42440d4c0..0000000000 --- a/tests/data/rational/rational.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: rational -include: ../../../src/ . diff --git a/tests/data/rational/run b/tests/data/rational/run index f6e7c9b3c0..b81665946a 100644 --- a/tests/data/rational/run +++ b/tests/data/rational/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 f6e7c9b3c0..0ac4190b78 100644 --- a/tests/data/trie/run +++ b/tests/data/trie/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "trie" diff --git a/tests/data/trie/trie.agda-lib b/tests/data/trie/trie.agda-lib deleted file mode 100644 index 1e1ae6dec2..0000000000 --- a/tests/data/trie/trie.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: trie -include: ../../../src/ . diff --git a/tests/monad/counting/counting.agda-lib b/tests/monad/counting/counting.agda-lib deleted file mode 100644 index 34e6fcee78..0000000000 --- a/tests/monad/counting/counting.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: counting -include: ../../../src/ . diff --git a/tests/monad/counting/run b/tests/monad/counting/run index f6e7c9b3c0..24e733e240 100644 --- a/tests/monad/counting/run +++ b/tests/monad/counting/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "counting" diff --git a/tests/monad/fibonacci/fibonacci.agda-lib b/tests/monad/fibonacci/fibonacci.agda-lib deleted file mode 100644 index 48fa8830d1..0000000000 --- a/tests/monad/fibonacci/fibonacci.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: fibonacci -include: ../../../src/ . diff --git a/tests/monad/fibonacci/run b/tests/monad/fibonacci/run index f6e7c9b3c0..4d4b6bf028 100644 --- a/tests/monad/fibonacci/run +++ b/tests/monad/fibonacci/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "fibonacci" diff --git a/tests/monad/pythagorean/pythagorean.agda-lib b/tests/monad/pythagorean/pythagorean.agda-lib deleted file mode 100644 index d434562aa8..0000000000 --- a/tests/monad/pythagorean/pythagorean.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: pythagorean -include: ../../../src/ . diff --git a/tests/monad/pythagorean/run b/tests/monad/pythagorean/run index f6e7c9b3c0..f35fce4c89 100644 --- a/tests/monad/pythagorean/run +++ b/tests/monad/pythagorean/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 f6e7c9b3c0..e29253c133 100644 --- a/tests/monad/tcm/run +++ b/tests/monad/tcm/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "tcm" diff --git a/tests/monad/tcm/tcm.agda-lib b/tests/monad/tcm/tcm.agda-lib deleted file mode 100644 index c7559e3dc4..0000000000 --- a/tests/monad/tcm/tcm.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: tcm -include: ../../../src/ . diff --git a/tests/reflection/assumption/assumption.agda-lib b/tests/reflection/assumption/assumption.agda-lib deleted file mode 100644 index f5d7d392ed..0000000000 --- a/tests/reflection/assumption/assumption.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: assumption -include: ../../../src/ . diff --git a/tests/reflection/assumption/run b/tests/reflection/assumption/run index f6e7c9b3c0..c1050c39b7 100644 --- a/tests/reflection/assumption/run +++ b/tests/reflection/assumption/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 c1cba66e6f..0000000000 --- a/tests/show/num/num.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: num -include: ../../../src/ . diff --git a/tests/show/num/run b/tests/show/num/run index f6e7c9b3c0..d09825bf26 100644 --- a/tests/show/num/run +++ b/tests/show/num/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "num" diff --git a/tests/show/reflection/reflection.agda-lib b/tests/show/reflection/reflection.agda-lib deleted file mode 100644 index 79ffa5c292..0000000000 --- a/tests/show/reflection/reflection.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: reflection -include: ../../../src/ . diff --git a/tests/show/reflection/run b/tests/show/reflection/run index f6e7c9b3c0..938c2c379a 100644 --- a/tests/show/reflection/run +++ b/tests/show/reflection/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 f6e7c9b3c0..61fd29c26c 100644 --- a/tests/show/tree/run +++ b/tests/show/tree/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 f659528634..0000000000 --- a/tests/show/tree/tree.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: tree -include: ../../../src/ . diff --git a/tests/standard-library-tests.agda-lib b/tests/standard-library-tests.agda-lib deleted file mode 100644 index 07abad7e4a..0000000000 --- a/tests/standard-library-tests.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: standard-library-tests -include: ../src/ . diff --git a/tests/system/ansi/ansi.agda-lib b/tests/system/ansi/ansi.agda-lib deleted file mode 100644 index 367219e74b..0000000000 --- a/tests/system/ansi/ansi.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: ansi -include: ../../../src/ . diff --git a/tests/system/ansi/run b/tests/system/ansi/run index 20143a4947..2ca1dc4e04 100644 --- a/tests/system/ansi/run +++ b/tests/system/ansi/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main hello world > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "ansi" diff --git a/tests/system/directory/directory.agda-lib b/tests/system/directory/directory.agda-lib deleted file mode 100644 index 6abd1b5e02..0000000000 --- a/tests/system/directory/directory.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: directory -include: ../../../src/ . 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 diff --git a/tests/system/directory/run b/tests/system/directory/run index f6e7c9b3c0..528b57abde 100644 --- a/tests/system/directory/run +++ b/tests/system/directory/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "directory" diff --git a/tests/system/environment/environment.agda-lib b/tests/system/environment/environment.agda-lib deleted file mode 100644 index bcc0d5b45c..0000000000 --- a/tests/system/environment/environment.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: environment -include: ../../../src/ . diff --git a/tests/system/environment/expected b/tests/system/environment/expected index 1f387d2af2..5923f67e28 100644 --- a/tests/system/environment/expected +++ b/tests/system/environment/expected @@ -1,3 +1,3 @@ -Main +stdlib-test-environment hello world hello back! diff --git a/tests/system/environment/run b/tests/system/environment/run index 20143a4947..68c4b3ee25 100644 --- a/tests/system/environment/run +++ b/tests/system/environment/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main hello world > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "environment" "hello world" diff --git a/tests/text/pretty/pretty.agda-lib b/tests/text/pretty/pretty.agda-lib deleted file mode 100644 index 8ec073abd7..0000000000 --- a/tests/text/pretty/pretty.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: pretty -include: ../../../src/ . diff --git a/tests/text/pretty/run b/tests/text/pretty/run index f6e7c9b3c0..fc4d8e6310 100644 --- a/tests/text/pretty/run +++ b/tests/text/pretty/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 cb42e692e3..0000000000 --- a/tests/text/printf/printf.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: printf -include: ../../../src/ . diff --git a/tests/text/printf/run b/tests/text/printf/run index f6e7c9b3c0..0dd6507ca2 100644 --- a/tests/text/printf/run +++ b/tests/text/printf/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ No newline at end of file +. ../../_config/config.sh +goldenTest "$1" "printf" 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..4f24d6402b 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 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 new file mode 100644 index 0000000000..a07ccbd4d6 --- /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 the bsiness up by moving to ¡hell! +She now sells her chisels by the shelter \ No newline at end of file diff --git a/tests/text/regex/regex.agda-lib b/tests/text/regex/regex.agda-lib deleted file mode 100644 index 1c33b14658..0000000000 --- a/tests/text/regex/regex.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: regex -include: ../../../src/ . diff --git a/tests/text/regex/run b/tests/text/regex/run index f6e7c9b3c0..c19ca4c1d7 100644 --- a/tests/text/regex/run +++ b/tests/text/regex/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 f6e7c9b3c0..5a4022629a 100644 --- a/tests/text/tabular/run +++ b/tests/text/tabular/run @@ -1,5 +1,2 @@ -$1 --compile-dir=../../_build -c Main.agda > log -./../../_build/Main > output - -rm ../../_build/Main -rm ../../_build/MAlonzo/Code/Main* \ 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 de85f156b1..0000000000 --- a/tests/text/tabular/tabular.agda-lib +++ /dev/null @@ -1,2 +0,0 @@ -name: tabular -include: ../../../src/ .