Fix or disable broken test cases

[nad]

Some test cases depend on the Agda library, and may or may not work depending on what is installed. I've found the following examples in test/interaction:

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/interaction/Issue720.hs#L7

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/interaction/Issue983.hs#L6

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/interaction/Issue1232.hs#L6

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/interaction/Issue4835/Count.hs#L7-L19

The CI tests often fail because Agda.Version is not found, so I think we should fix this problem soon:

• The test cases for issues #983 and #1232 use Agda.Version in order to remove a certain file in a _build directory. Perhaps we could just leave the file there.
• The test case for issue #720 removes an interface file before it is reloaded. The original test case touched the source file, perhaps that is sufficient.
• The test case for issue #4835 imports lots of Agda modules and counts the number of occurrences of a certain module identifier in an interface. Perhaps we could remove this test case. An alternative would be to use Cabal to handle the dependency.

[nad]

I found three more examples:

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/Issue1168.hs#L14-L21

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/PrettyInterface.hs#L17-L29

https://github.com/agda/agda/blob/9a29f3a1f5e24c818bdabbf2c17d0f79887aa8b4/test/api/ScopeFromInterface.hs#L27-L41

When I run make api-test I get the following output:

======================================================================
========== Successful tests using Agda as a Haskell library ==========
======================================================================
make[1]: Entering directory '[…]/test/api'
rm -f *.agdai *.hi *.o
make[1]: Leaving directory '[…]/test/api'
make[1]: Entering directory '[…]/test/api'
[…]/dist-2.6.3-ghc-9.0.2/build/agda/agda -v0 --no-libraries Issue1168.agda
[…]/ghc -Wall -Werror -package Agda-2.6.3 -o […]/Issue1168 Issue1168.hs
Loaded package environment from […]/.ghc/x86_64-linux-9.0.2/environments/default
<command line>: cannot satisfy -package Agda-2.6.3
    (use -v for more information)
make[1]: *** [Makefile:14: Issue1168.api] Error 1
rm Issue1168.agdai
make[1]: Leaving directory '[…]/test/api'
make: *** [Makefile:539: api-test] Error 2

[nad]

The API test cases could perhaps be integrated into the agda-tests program.

[JacquesCarette]

My experience (from long ago as a professional software developer) was that disabling tests seemed to always come back to bite us, because someone re-broke the thing that ways being tested. Even changing the way the test was conducted sometimes defeated the point of the test, as the original method was a better trigger of the bad behaviour! [Unfortunately, the time elapsed between the test being disabled and the issue re-occurring seemed to be on the order of 7 years!]

When I was a manager of a group of devs, we sometimes spent a lot of time figuring out how to rewrite some tests so as to keep them. It's kind of a fun dual to 'debugging'!

More constructively: these really do seem to test meaningful Agda things, so perhaps what's the issue is that the current tests are not sufficiently 'MWE'? The bug being tested for many in your first report doesn't seem to actually involve the library in an essential way.

[As always: I'm a strong believer in weighing advice by the amount of effort the giver-of-advice is willing to spend on said advice. So, in my case, 10 minutes, though it is based on real experience. ]

[nad]

Another broken test case:

$ make size-solver-test
======================================================================
================= Installing the size-solver program =================
======================================================================
make[1]: Entering directory '[…]/src/size-solver'
cabal v1-install --enable-tests  --builddir=./dist-2.6.3-ghc-9.0.2 -fenable-cluster-counting --ghc-options="+RTS -M6G -RTS" 
Resolving dependencies...
Configuring size-solver-0.2016.7.13...
Preprocessing executable 'size-solver' for size-solver-0.2016.7.13..
Building executable 'size-solver' for size-solver-0.2016.7.13..
[1 of 2] Compiling Parser           ( Parser.hs, dist-2.6.3-ghc-9.0.2/build/size-solver/size-solver-tmp/Parser.o )
[2 of 2] Compiling Main             ( Main.hs, dist-2.6.3-ghc-9.0.2/build/size-solver/size-solver-tmp/Main.o )
Linking ./dist-2.6.3-ghc-9.0.2/build/size-solver/size-solver ...
Installing executable size-solver in […]/bin
Completed    size-solver-0.2016.7.13
Warning: could not create a symlink in […]/bin for
size-solver because the file exists there already but is not managed by cabal.
You can create a symlink for this executable manually if you wish. The
executable file has been installed at
[…]/bin/size-solver
make[1]: Leaving directory '[…]/src/size-solver'
======================================================================
================== Testing the size-solver program ===================
======================================================================
make[1]: Entering directory '[…]/src/size-solver'
shelltest --color --precise test/succeed.test
:test/succeed.test:1: [Failed]
ERROR: user error (/bin/sh: 1: dist/build/size-solver/size-solver: not found
 Command: 'dist/build/size-solver/size-solver < test/succeed/Issue2415.txt' Exit code: 127)
:test/succeed.test:2: [Failed]
ERROR: user error (/bin/sh: 1: dist/build/size-solver/size-solver: not found
 Command: 'dist/build/size-solver/size-solver < test/succeed/Issue2558.txt' Exit code: 127)

         Test Cases  Total      
 Passed  0           0          
 Failed  2           2          
 Total   2           2          
make[1]: *** [Makefile:26: test] Error 1
make[1]: Leaving directory '[…]/src/size-solver'
make: *** [Makefile:581: size-solver-test] Error 2

I don't see why this test case needs to be part of make test.

[jespercockx]

This is not relevant to a specific release of Agda so I've removed the milestone.

[andreasabel]

Yeah, these test should be upgraded to use cabal v2 idioms.

[andreasabel]

Switching to v2-cabal and write-ghc-environment-files: always should fix these issues.

E.g. after a cabal build with write-ghc-environment-files: always the following succeeds:

make AGDA_BIN=$(cabal list-bin agda) interaction