@alexarice Do we have all agda libraries on CI? Or could it be that I accidentally break one this way?

Indeed this broke the generic package. I'll try and update the agda test in a way that it would have caught this.

This test now shows that generic doesn't build.

I don't understand why there is no CI failure. When I do nix-build nixos/tests/agda.nix, it fails with the error message described here:

effectfully/Generic#5

CI doesn't run the tests by default. I'm also not sure building every agda package in the tests is a good idea.
Edit: Maybe CI has changed but it seems it is trying to run passthru.tests which we have not set I believe

Given that my understanding is that it only breaks the one library, we could just go ahead

I'd prefer not to modify the test here, and likely not in this way. I don't think anything else checks that all their packages build.

But we should add some test somewhere that builds all packages, do you agree? Where could such a test reside?

Don't update yet and wait for some things to catch up

I guess that's fine as well. As far as I could see, generic is the only package that failed, and it's probably fairly easy to fix.

Add a standard-library_1.3 package

I think that's a great option as well. I can make the standard library builder generic and call it twice, with both versions.

I'd go for first waiting a bit until all packages work with 1.4. It's an interesting experiment to see whether there is enough motivation in the community to stay coherent. If it works out fine, then great. If not, we can wonder about the other options.

I'd prefer not to modify the test here, and likely not in this way. I don't think anything else checks that all their packages build.

But we should add some test somewhere that builds all packages, do you agree? Where could such a test reside?

I'm not sure it's usual to have a test like this, but if we did perhaps it should be a standard library test rather than an agda test

I fixed generic here: effectfully/Generic#6

Maybe it gets released soon.

I'm not sure it's usual to have a test like this, but if we did perhaps it should be a standard library test rather than an agda test

I'm also not sure, but it doesn't seem wasteful to me. The packages need to be built anyways for the cache, and it would be nice to have some signal if something breaks. In Haskell, this is done by stackage. I'm imagining that nixpkgs could step in for the corresponding task in the Agda world. Given that it's just a handful curated packages, it seems feasible.

Anyways, I guess it's a separate issue. I opened one: #98209

Indeed a pleasantly fast response, on generic. But agda-categories fails as well.

This is unsurprising, and it took a bit of work to get a release last time

Yes, they seem to have released it several times until they got it right. I think nixpkgs can help there because we can build one consistent package set.

With agda/agda-categories#207 merged all nonbroken packages should compile again.

@alexarice Is it ok if the updated other packages (generic and agda-categories) don't have a release tag? Or should we only update them when they release a new version?

That's a good spot, is this change post 1.4?

That's a good spot, is this change post 1.4?

Yes, it seems that starting at 1.5 and going forward they will have versioning in the package name.

I think the name of the agda package here should not have a version number, i.e. it should be agdaPackages.agda-stdlib and not agdaPackages.agda-stdlib-1.4. The convention for the latter is that sometimes, old legacy versions or new preview versions are added. But the released, up-to-date version should not have a version number.

We'll have to add libraryName = "${pname}-${version}" from next release onwards but I think this one is unaffected

Let me re-evaluate which packages are broken, and mark them broken. Both agda-categories and Generic have released compatible versions, I'll update.

No other packages are broken. I updated agda-stdlib, agda-categories, generic to latest released versions.

I believe we should merge this as-is, and not bump the other packages. That should be a separate MR, if at all necessary.

/marvin opt-in
/status needs_reviewer

Hi! I'm an experimental bot. My goal is to guide this PR through its stages, hopefully ending with a merge. You can read up on the usage here.

I think this could all just be one commit really

I always thought that separate package updates should be separate commits. Otherwise we can't follow the commit message format in https://github.com/NixOS/nixpkgs/blob/master/.github/CONTRIBUTING.md.

I think there is a precedent for package sets that mutually break eachother being updated in one commit. See haskellPackages, emacsPackages etc. I don't mind too much either way though

Edit: These are updated automatically though

Ah I didn't know. I prefer committing each update separately, tbh.

Sure, can we rebase out the fix whitespace commit in any case

Sure, can we rebase out the fix whitespace commit in any case

Done.

Reminder: Please review!

This Pull Request is awaiting review. If you are the assigned reviewer, please have a look. Try to find another reviewer if necessary. If you can't, please say so. If the status is not accurate, please change it. If nothing happens, this PR will be put back in the needs_reviewer queue in one day.

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/prs-already-reviewed/2617/255