We already made the necessary changes as part of the ghc-8.8 support (#3725) unless I'm very much mistaken. At least I've been using cabal-3.0.0.0 without issue since then. Is the ghc-8.8 Travis job not using 3.0.0.0?

The Travis job for GHC 8.8.1 is using caba-install 2.4.1.0.

I got an error when running cabal install in a fresh repository. I'll report the error later.

cabal-3.0 works well to me.

The following one is built with GHC 8.8.1 and cabal 3.0

https://travis-ci.org/L-TChen/agda/jobs/614341754

The above job don't use cabal-install but stack.

I got an error when running cabal install in a fresh repository.

You have to use cabal v1-install.

Stack has not been tested with GHC versions above 8.6, and using 8.8.1, this may fail
Stack has not been tested with Cabal versions above 2.4, but version 3.0.0.0 was found, this may fail

If I was not mistaken, stack uses cabal to install packages ...
https://docs.haskellstack.org/en/stable/faq/#what-is-the-relationship-between-stack-and-cabal

I think stack uses Cabal the library, but it doesn't use cabal-install the program.

You have to use cabal v1-install.

I guess. Are you planning to update the user documentation for taking care of the different versions of cabal-install?

Running cabal-install the first error I got is

$ cabal install
cabal: filepath wildcard 'doc/user-manual.pdf' does not match any files.

This is also the error in Travis when using GHC 8.8.1 and cabal-install 3.0.0.0.

I think the idea is to eventually deprecate v1-install, so I guess we should at some point make v2-install work.

I'm building Agda with cabal 3.0.0.0 for weeks. It always work

I'm building Agda with cabal 3.0.0.0 for weeks. It always work

Can you make a GH Actions workflow using cabal 3.0 with v2-install? Just make sure that Agda is compatible.

How did you make the stack one? Is it just porting the .travis.yml?

Almost. GHC, cabal (2.0-3.0) and stack are all preinstalled already, so it should be simpler.

https://help.github.com/en/actions/automating-your-workflow-with-github-actions/software-installed-on-github-hosted-runners

I'm building Agda with cabal 3.0.0.0 for weeks. It always work

Then perhaps the makefile could be updated to use install instead of v1-install. (Just dropping the v1- prefix does not work.)

It seems that by removing doc/user-manual.pdf from extra-source-files in Agda.cabal, it actually compiles https://github.com/agda/agda/commit/e956e9d356750c0fe92477c3ecbca70edaf56f2b/checks?check_suite_id=328447539

I haven't run the test suites with the compiled binary, though. Adding this workflow might be a good idea before revising Makefile? I am not able to revise Makefile this year anyway ...

It seems that by removing doc/user-manual.pdf from extra-source-files in Agda.cabal, it actually compiles.

Yes. Please remove it. I'll add it back in the releases branches.

To migrate to v2-cabal these problems remain for me:

• make type-check: The v1-solution passing --ghc-options=-fno-code does not work with v2-cabal, as it wants then to reinstall all the dependencies (Explicitly support building with -fno-code haskell/cabal#1176, v2-cabal: Don't rebuild dependencies when -O0 or -fno-code is supplied as --ghc-options haskell/cabal#7368)
• make install-bin: cabal install after cabal build recompiles Agda from scratch, since it compiles from the sdist-tarball. One could try to work around this by writing a script that copies the relevant bits from the build tree to the --installdir. (cabal install run immediately after cabal build unnecessarily rebuilds the project haskell/cabal#6919 (comment))

Could you clarify the status of this issue/effort? How long till there's a version of Makefile (or of mk/cabal.mk) that uses v2- commands?

If one doesn't want to mess with his Haskell environment using cabal v1- commands, how can one build and install the current (master) Agda from the source (cloning this repo), if one wants to also run tests?

Should the following work (in sequence as typed):

• cabal build | tee >(copy-bins.awk)
• make bugs
• make test
  ?

My latest efforts are at:

• cabal build | tee >(copy-bins.awk)

If you have a recent version of cabal-install, then you can perhaps use cabal list-bin to find the path to the executable.

Also, please take a look at haskell/cabal#7693 - perhaps it would be helpful here, or you might be able to give some useful feedback there.

#4216 (comment) looks like haskell/cabal#7679

#4216 (comment) looks like haskell/cabal#7679

They are two different aspects of the same problem:

• cabal list-bin cabal-tests (and others) fails with "No or multiple targets given" haskell/cabal#7679 is about how to make Cabal build and install dependencies even when --enable-tests is set.
• Support cabal-install 3.0.0.0 in the Makefile #4216 (comment) is about how to modify Agda installation and testing process to avoid triggering the problem that Cabal introduces for v2- commands.

As asked here - what's the point of having --only-dependencies in the install command? Since we install the generated binaries before running tests anyway - why not ditch that parameter altogether???

As asked here - what's the point of having --only-dependencies in the install command? Since we install the generated binaries before running tests anyway - why not ditch that parameter altogether???

Dunno, maybe @asr can say more.

I can see a use for --only-dependencies in the following cases:

• CI: First install dependencies, cache them for the next time, then install Agda but don't cache it. (This is what is often done in the github workflows.)
• Developer: Install dependencies with optimization on, but build Agda without optimizations for quick testing. (This at least made sense with v1-cabal, the situation with v2-cabal is more confusing.)

1. CI: I don't think dependencies that did not change themselves, would be rebuilt - therefore, no need to worry about them.
2. Developer: I understand the logic, but I'm pretty sure that (unlike in C/C++) you cannot build dependencies with one set of flags, and then build the "main" package with another set of flags without having all the dependencies rebuilt. Difference in the flag set can be minimal - one flag would be sufficient to force the rebuild/recompile.

• CI: First install dependencies, cache them for the next time, then install Agda but don't cache it. (This is what is often done in the github workflows.)

As for CI, the main benefit of using --only-dependencies, I think, is to navigate the error information easier.

OK, so having had all this discussion and observing what Cabal maintainers got to say about this, where are we regarding move to cabal v2- build?

Update

It looks like the sequence for cabal v2-... should be

1. cabal v2-build --enable-tests --only-dependencies (optional, I don't fully understand what separating this step accomplishes, given that CI probably builds everything)
2. cabal v2-build --enable-tests
3. actually running tests - and here's my stumbling block: how do I get all the Agda tests to run, given that I know where agda, agda-mode, and agda-tests binaries are?
4. finally, cabal v2-install that will place the Agda binaries into the global store ~/.cabal/bin and ~/.cabal/store

Do you concur? If so, how to deal with (3) above?

Update 2

Specifically, what scripts and mk/*.mk files do I need to modify, to get make test working with this new build? Assuming that I know the locations of agda, agda-mode, and agda-tests?