Closed VojtechStep closed 1 year ago
Thanks, but I'll have to close. Since Agda is implemented in Haskell, it is available on Hackage. As such, it is automatically updated together with all other Haskell packages. See https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/haskell-modules/HACKING.md for details of that process. The fact that Agda is updated as part of the Haskell packages isn't documented AFAIK, so feel free to document that in https://nixos.org/manual/nixpkgs/stable/#maintaining-the-agda-package-set-on-nixpkgs and ping me on the PR.
I thought I'd open an issue, because the last update PR https://github.com/NixOS/nixpkgs/pull/213896 also bumped versions of the packaged Agda libraries. Will that not block the Agda update? @turion
No, it should not necessarily. If everything goes well, the agda libraries still compile after an agda update, and nothing is blocked. Worst case, some agda libraries don't compile, and will be marked broken. Then people can fix them independently of haskell updates.
In https://github.com/NixOS/nixpkgs/pull/213896#issuecomment-1424078194 I meant that it's a good idea to find out early if the agda packages are all fit for the new agda version, and therefore it's a good idea to make a branch with a new agda version and test them. That way, we don't have to mark agda libraries as broken when agda is updated. But I wouldn't merge such a PR ahead of haskell updates if it's not necessary.
In other words: If you want to bump Agda 2.6.4 and make sure all/some specific libraries still work, that's very welcome as a PR :) I might recommend then to wait merging that branch into haskell-updates
as soon as 2.6.4 is on stackage, and not earlier.
And I personally won't start bumping the version myself. But don't let that be a deterrent for anyone else :)
Thanks!
Just for your information, Agda 2.6.4.1 is already in haskell-updates and the Agda libraries we ship in nixpkgs are compatible with Agda 2.6.4.1.
Notify maintainers
@abbradar @iblech @turion
Note for maintainers: Please tag this issue in your PR.