diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index a40fe804ad..750b2e2988 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: ######################################################################## @@ -47,7 +48,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' @@ -98,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: | @@ -113,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 }} @@ -168,8 +169,7 @@ jobs: - name: Golden testing run: | - ${{ env.CABAL_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 e744f066cc..85fc330888 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)" only=$(only) fix-whitespace: cabal exec -- fix-whitespace diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index 43bbd3037e..e12df07317 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -204,9 +204,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" ∷ [] @@ -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/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 new file mode 100644 index 0000000000..989c9478fa --- /dev/null +++ b/tests/README.md @@ -0,0 +1,56 @@ +# 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 + +## 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 +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 cf9af60245..16d29516d1 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/ .