building tests with cabal

[rdck]

What's the correct way to build the tests with cabal?

AFAIK, the install-bin target should create agda-tests in the build directory, if everything is working correctly. But it doesn't. I noticed that there aren't any test suites defined in Agda.cabal, but I'm not sure if that's the reason.

Here's the log for make test:

cd src/fix-agda-whitespace && cabal v1-clean && cabal v1-build
======================================================================
===================== Suite of successful tests ======================
======================================================================
make[1]: Entering directory '/home/river/sources/op/aports/testing/agda/src/agda-2.6.1.3/test/Common'
cleaning...
Bool.agda
Char.agda
Coinduction.agda
Equality.agda
Resolving dependencies...
Configuring fix-agda-whitespace-0.0.4...
Float.agda
Preprocessing executable 'fix-agda-whitespace' for fix-agda-whitespace-0.0.4..
Building executable 'fix-agda-whitespace' for fix-agda-whitespace-0.0.4..
[1 of 1] Compiling Main             ( FixWhitespace.hs, dist/build/fix-agda-whitespace/fix-agda-whitespace-tmp/Main.o )
Linking dist/build/fix-agda-whitespace/fix-agda-whitespace ...
IO.agda
======================================================================
======================= Suite of failing tests =======================
======================================================================
bash: line 1: /home/river/sources/op/aports/testing/agda/src/agda-2.6.1.3/dist/dist-sandbox-6c72f0e1/build/agda-tests/agda-tests: No such file or directory
make: *** [Makefile:280: fail] Error 127
make: *** Waiting for unfinished jobs....
Integer.agda
Irrelevance.agda
Issue481ParametrizedModule.agda
Issue964/UnsolvedMetas.agda
Level.agda
List.agda
MAlonzo.agda
Maybe.agda
Nat.agda
Prelude.agda
Product.agda
Reflection.agda
Size.agda
String.agda
Sum.agda
Unit.agda
make[1]: Leaving directory '/home/river/sources/op/aports/testing/agda/src/agda-2.6.1.3/test/Common'
bash: line 1: /home/river/sources/op/aports/testing/agda/src/agda-2.6.1.3/dist/dist-sandbox-6c72f0e1/build/agda-tests/agda-tests: No such file or directory
make: *** [Makefile:274: succeed] Error 127
>>> ERROR: agda: check failed

I'm on the latest release (2.6.1.3).

[andreasabel]

agda-tests is only for running the internal test suite, i.e., QuickCheck tests. The other tests are run, as you correctly tried, via make test.
It seems that your make does things in parallel, at least the log is wildly mixing different execution threads, so it is hard to make sense of it. What is the log with a sequential execution of make test?

[asr]

I noticed that there aren't any test suites defined in Agda.cabal.

The tests are not included in the released version.

[andreasabel]

@asr: Is there a strong reason why cabal test cannot run the testsuite?

If I try this, I get an error that AGDA_BIN is not set. Is there maybe a way to get the agda binary that was created in connection with cabal test?

On a practical side, running the whole testsuite may be too much, but cabal test could at least run a selection of tests.

[mouse07410]

This problem is only a tip of the iceberg, and reflects that Cabal places the built binaries to where the subsequent tests don't look for it - aka, can't find.

Here's my way of solving it by creating a wrapper shell script that does the right magic for the complete rebuild. It ensures (by setting appropriate env vars and removing stale binaries) that at least the right binaries are correctly located and used:

#!/bin/bash

DATE_START="`date`"

export GHC_ENVIRONMENT=-

VER=`head -4 mk/versions.mk | grep VERSION | cut -f2 -d '='`
DAT=`date "+%Y-%m-%d"`
GHCVER=`ghc --numeric-version`

HOM="${PWD}"
if [[ "$OSTYPE" == "darwin"* ]]; then
    # MacOS
    export AGDA_BIN=${HOM}/dist-${VER}-ghc-${GHCVER}/build/Agda/agda
    MAKE=gmake
else
    # Linux
    export AGDA_BIN=${HOM}/dist-${VER}-ghc-${GHCVER}/build/agda/agda
    MAKE=make
fi
export AGDA_TESTS=${HOM}/dist-${VER}-ghc-${GHCVER}/build/agda-tests/agda-tests

echo ""
echo "GHC_ENVIRONMENT: ${GHC_ENVIRONMENT}"
echo "AGDA_bin:   ${AGDA_BIN}"
echo "AGDA_TESTS: ${AGDA_TESTS}"
echo "CABAL_OPTS: ${CABAL_OPTS}"
echo ""

# Remove the leftovers from previous (successful) installs
# that may interfere with this build
find ~/.cabal/lib -name '*[Aa]gda*' -print -exec rm -rf {} \;
rm -f ~/.cabal/bin/AllNonAsciiChars ~/.cabal/bin/GenerateEverything

# Remove potentially stale "fix-whitespaces", as it's quicker to rebuild
# than to figure if it's built with the correct GHC and such
rm -rf ${HOM}/src/fix-whitespace/dist/build

# Remove stale size-solver from the past
rm -rf ${HOM}/src/size-solver/dist*

${MAKE} clean || true

${MAKE} install 2>&1 | tee make-out-${DAT}.txt
if [ $? != 0 ]; then
	echo "Agda-${VER} build failed!"
	exit 1
fi

${MAKE} bugs 2>&1 | tee make-bugs-${DAT}.txt
${MAKE} bugs 2>&1 | tee make-bugs-${DAT}.txt
time ${MAKE} test 2>&1 | tee make-test-${DAT}.txt 
if [ $? != 0 ]; then
        echo "Agda-${VER} tests failed!"
        exit 1
fi

${MAKE} user-manual-pdf 2>&1 | tee make-pdf-${DAT}.txt

DATE_END="`date`"
echo ""
echo "Start: ${DATE_START}"
echo "End:   ${DATE_END}"

#

[mouse07410]

Note that once you get through this issue (e.g., by adopting the above script), you'll have to apply the workarounds from #5528 in order for your tests to actually run and pass.

[andreasabel]

agda-tests is only for running the internal test suite, i.e., QuickCheck tests. The other tests are run, as you correctly tried, via make test.

Er, this was many years ago, before @phile314 integrated other parts of the test suite into agda-tests. :$

I started working on having cabal test run parts of the test suite. I think it would make sense that this only runs a small fraction, just to see whether Agda is operational. Could be as little as type-checking a "hello world" program or the like...

[mouse07410]

I'd say, as long as the entire build and test-run works with Cabal, without the need to use Stack - it's not crucial whether make is involved or not. make test is simple enough - I wouldn't kill myself over trying to port it to cabal test.

[andreasabel]

Yeah, maybe a standalone cabal test isn't possible due to haskell/cabal#7577 (comment).
Maybe cabal install --run-tests can be made to work, but this isn't a good developer option, as cabal install rebuilds from scratch, see haskell/cabal#6919. But actually, cabal install --run-tests doesn't work either, see haskell/cabal#7267.

[andreasabel]

In PR #5536 I set up a CI (ubuntu, macOS) that runs cabal test after cabal install.
Atm, too much of the testsuite is included to have it serve as a simple check that Agda is operational. However, the technology is in place now, and if there is interest, we can design a sensible subset of the testsuite to be run with cabal test.

A flaw in the ointment is that cabal {v1|v2}-install Agda --run-tests will not run the tests. However, a small testsuite could be included still; it could at least be run by stack.

[mouse07410]

As I said earlier, I see a lot of value in being able to build using Cabal without Stack (just like it is important to be able to build using Stack without Cabal). I also think that switching to cabal v2-install would be a huge advantage over the current cabal v1-install.

But I see little benefit in replacing make test with cabal test or cabal install --run-tests.

make (already) does a good enough job, as far as I'm concerned, and I suspect many users would concur.

[andreasabel]

@mouse07410 wrote:

switching to cabal v2-install

The new CI (cabal-test) in this PR ensures that cabal v2-install and cabal v2-test succeed without build errors (such as you experience). The existing Build (cabal) workflow already tested cabal v2-build.

Atm, we cannot fully switch the Makefile to v2 since e.g. the type-check goal does not work sensibly with v2-cabal (see haskell/cabal#1176).

[mouse07410]

Atm, we cannot fully switch the Makefile to v2 since . . .

Understood. This was not intended as a criticism - you guys are doing good IMHO! - but as an attempt to "help" with prioritization of efforts.