Agda 2.6.4 updates

[ncfavier]

#262645 bumps Agda to 2.6.4. This PR updates some Agda packages to work with 2.6.4, and marks the broken ones as broken.

Tested with nixosTests.agda and agda.tests.allPackages.

[turion]

Thanks a lot! It would be great if we could have some grace period to give the packages some time to update, open upstream issues and ping maintainers. I find that marking libraries as broken should only be the last measure, when we are certain that we cannot expect timely upstream fixes.

[alexarice]

Thanks a lot! It would be great if we could have some grace period to give the packages some time to update, open upstream issues and ping maintainers. I find that marking libraries as broken should only be the last measure, when we are certain that we cannot expect timely upstream fixes.

I don't think we have this option, as Agda automatically updates as part of the haskell package set to my knowledge

[ncfavier]

Right, the grace period would have to delay the scheduled merge of haskell-updates. As soon as that branch is merged into master, those libraries will be broken, so marking them broken is just saving build time.

I don't think enough people care about agda-prelude and functional-linear-algebra to justify that. I'll report the issues upstream though.

[turion]

Yes we do, the haskell updates branch is not merged immediately, there is some time until it is merged. If we can make progress with broken packages in that time, we can merge them unbroken.

[turion]

Ah ok, I see your point. So we mark them broken and try to fix them while haskell-updates is stabilized. So it is always in a mergeable state and haskell-updates is not delayed. That's a good process.

Then I think the only thing left to do is ping maintainers for the broken packages.

CC @laMudri @ryanorendorff

[alexarice]

I think I've asked this before, but is it completely unreasonable to maintain Agda outside of the main haskell package set, so that we can choose when to update it/ potentially support multiple versions?

[turion]

but is it completely unreasonable to maintain Agda outside of the main haskell package set, so that we can choose when to update it/ potentially support multiple versions?

If it's easy enough to decouple from the Haskell package set sufficiently then I think this is a great idea. But since Agda itself is written in Haskell, there are going to be some dependencies. We can fix an agda version or several in pkgs/development/haskell-modules/configuration-hackage2nix/main.yaml, and as long as these work with the rest of the Haskell package set, everything is fine. We'd still need to keep the compatibility matrix of agda libraries somewhere. Would you want to have one version of every agda library per agda version, or one agda-global version of every library?

[turion]

@ofborg build agda.passthru.tests.allPackages