Upgrade Agda base version to 2.8.0-rc3

[jespercockx]

This is a first attempt at upgrading the Agda base version to 2.8.0 (well currently the 3rd release candidate, but I don't expect much more to change). It compiles and runs the tests, however there are some things that should be addressed before merging:

• There are a few Haskell build files that show up in lib/containers/haskell/Test/Agda2Hs after running make test. We might need these files but I don't think it's the right place for them (and anyway it's strange that they only show up now and not earlier). @HeinrichApfelmus could you please take a look?
• There is a regression in three test cases where a function gets inlined that previously didn't. Specifically:
  • test/golden/Issue302.hs
  • test/golden/Superclass.hs
  • test/golden/Test.hs
• There's another regression (I think) in test/golden/UnnamedVar.err which just reports UNEXPECTED_SUCCESS where it didn't report anything before.
• The error messages now contain a label for the error, but currently most of them are set to GenericError or GenericDocError. We should make use of CustomBackendError instead.
• In src/Main.hs I set the two new fields backendInteractTop and backendInteractHole to Nothing, but perhaps there's something better we could do there.
• The version of the Agda dependency should be updated to 2.8.0 once it is released on Hackage (and the source-repository-package field should be removed from cabal.project).

(All of this reminds me again of #153: we really need a better test infrastructure.)

[jespercockx]

If any nix experts know how to make the Nix CI pass with a custom commit from Github, please let me know (or push directly to this branch). Otherwise I will just ignore it until we have a proper Agda release.

[omelkonian]

There might be some weird interaction with Nix here. @liesnikov @HeinrichApfelmus?

[HeinrichApfelmus]

Removing --local-interfaces does make the agda2hs wrapper more compatible with agdaPackages from nixpkgs, though I do not know whether this makes it fully compatible.

In any case, the proper fix would be to have agda2hs provide its own mkDerivation function, as implemented in #407 .

[jespercockx]

The reason why I removed --local-interfaces is simply because it is no longer supported by the new release of Agda (see https://github.com/agda/agda/blob/ef912c68fd329ad3046d156e3c1a70a7fec19ba1/CHANGELOG.md?plain=1#L76)

[jespercockx]

I converted all errors to use CustomBackendError instead of Generic(Doc)Error. This has the nice side effect that all error messages are now automatically prepended by agda2hs: , which makes it a lot easier to determine whether a given error comes from agda2hs or Agda itself.

[jespercockx]

@HeinrichApfelmus Currently the two new agda2hs libraries are named base and containers, but I believe these are a bit too generic. Do you agree with renaming them to agda2hs-base and agda2hs-containers?

[HeinrichApfelmus]

Currently the two new agda2hs libraries are named base and containers, but I believe these are a bit too generic. Do you agree with renaming them to agda2hs-base and agda2hs-containers?

I don't mind either way. I was thinking that in a dream future where every package on Hackage has an equivalent in agda2hs, it would be cumbersome to prefix every package name foo to agda2hs-foo.

[HeinrichApfelmus]

If any nix experts know how to make the Nix CI pass with a custom commit from Github, please let me know (or push directly to this branch). Otherwise I will just ignore it until we have a proper Agda release.

I have added an incantation that pulls in the Agda-2.7.20250601 candidate package from Hackage. Unfortunately, this incantation currently breaks the nix develop shell. 🤔

[jespercockx]

I have added an incantation that pulls in the Agda-2.7.20250601 candidate package from Hackage. Unfortunately, this incantation currently breaks the nix develop shell. 🤔

Perhaps it's a problem that the cabal.project pulls the version from Github while your Nix magics get the version from Hackage. Or does the Nix CI ignore cabal.project completely?

Anyway, I'm fine with waiting to merge this PR until Agda 2.8.0 is officially released, which will hopefully make the problem disappear.

[HeinrichApfelmus]

Perhaps it's a problem that the cabal.project pulls the version from Github while your Nix magics get the version from Hackage. Or does the Nix CI ignore cabal.project completely?

The current Nix CI ignores cabal.project completely. 😅

Anyway, I'm fine with waiting to merge this PR until Agda 2.8.0 is officially released, which will hopefully make the problem disappear.

Most likely not without issues, though — this will require the inclusion of Agda 2.8.0 in nixpkgs, and then an update of the nixpkgs pin in flake.nix. For some reason that I do not understand, the last step fails on my aarch64-darwin machine.

[HeinrichApfelmus]

If any nix experts know how to make the Nix CI pass with a custom commit from Github, please let me know (or push directly to this branch). Otherwise I will just ignore it until we have a proper Agda release.

I have added an incantation that pulls in the Agda-2.7.20250601 candidate package from Hackage. Unfortunately, this incantation currently breaks the nix develop shell. 🤔

I managed to fix the incantation, the Nix CI now passes.