The test run succeeded just fine! :-)

However, I noticed a problem with the categories library. After upgrading to stdlib 1.5, its compilation fails with:

 Checking Categories.Adjoint.Instance.0-Truncation (/build/source/src/Categories/Adjoint/Instance/0-Truncation.agda).
  Checking Categories.Category.Construction.0-Groupoid (/build/source/src/Categories/Category/Construction/0-Groupoid.agda). 
  Checking Categories.Category.Instance.Groupoids (/build/source/src/Categories/Category/Instance/Groupoids.agda).
  Checking Categories.Functor.Instance.0-Truncation (/build/source/src/Categories/Functor/Instance/0-Truncation.agda).
 Checking Categories.Adjoint.Instance.01-Truncation (/build/source/src/Categories/Adjoint/Instance/01-Truncation.agda).
  Checking Relation.Binary.OrderMorphism (/nix/store/0wbmxylcp4mjm40ghj6rf7d1lhafly9s-standard-library-1.5/src/Relation/Binary/OrderMorphism.agda).
Failed to write interface /nix/store/0wbmxylcp4mjm40ghj6rf7d1lhafly9s-standard-library-1.5/src/Relation/Binary/OrderMorphism.agdai.
/build/source/src/Categories/Adjoint/Instance/01-Truncation.agda:11,1-60
/nix/store/0wbmxylcp4mjm40ghj6rf7d1lhafly9s-standard-library-1.5/src/Relation/Binary/OrderMorphism.agdai:
openBinaryFile: permission denied (Permission denied)
builder for '/nix/store/98q18lp471h0mzj79afxqspz82i1375d-agda-categories-0.1.4.drv' failed with exit code 1
cannot build derivation '/nix/store/ippc4pcj16qmdsa879qb9f7cp63mgi7a-libraries.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/3crj84m1avs17ljgsm4v6nby16y0272m-agdaWithPackages-2.6.1.2.drv': 1 dependencies couldn't be built
error: build of '/nix/store/3crj84m1avs17ljgsm4v6nby16y0272m-agdaWithPackages-2.6.1.2.drv' failed

You should be able to reproduce this with

$ nix-shell -I nixpkgs=https://github.com/iblech/nixpkgs/archive/patch-agdastdlib15.tar.gz -p "agda.withPackages (p: [ p.standard-library p.agda-categories ])"

I will try to look into that tomorrow (but can't promise).

Edit: Aha. This is because Relation.Binary.OrderMorphism has been deprecated and removed from std-lib's Everything.agda. As a consequence, we are no longer precompiling it; but on-demand compilation triggered by the categories library fails because of missing write permissions.

Edit²: I propose we upgrade standard-library to 1.5 (hence merge this pull request), but then also submit a pull request to upstream agda-categories, rendering it compatible with the new standard-library, and then update our package for agda-categories. What do you think?

Edit: Aha. This is because Relation.Binary.OrderMorphism has been deprecated and removed from std-lib's Everything.agda. As a consequence, we are no longer precompiling it; but on-demand compilation triggered by the categories library fails because of missing write permissions.

Yes, I agree that this is what happens.

Edit²: I propose we upgrade standard-library to 1.5 (hence merge this pull request), but then also submit a pull request to upstream agda-categories, rendering it compatible with the new standard-library, and then update our package for agda-categories. What do you think?

I think it's better to have it the other way around. The aim is to always have a working agda library set. Every package in the following set should build: lib.filterAttrs (name: value: (builtins.isAttrs value && builtins.hasAttr "isAgdaDerivation" value && value.isAgdaDerivation && !value.meta.broken)) agdaPackages

So the PR to agda-categories should go first. Maybe they'll merge it very quickly, maybe they'll even release a new version soon. If this happens within a few days, update that as well, and we can merge both together. If it takes longer, we can temporarily point nixpkgs to the fixed fork.

I would vote for holding off on this until agda-categories is ready

You can use #98209 (comment) to check whether all agda libraries build

@iblech Also, thanks a lot for helping to keep the agda package set up to date :)

Upstream issue: agda/agda-categories#242

3 libraries are incompatible with this update 🤭 let's see, hopefully they will all update soon

Aha. This is because Relation.Binary.OrderMorphism has been deprecated and removed from std-lib's Everything.agda. As a consequence, we are no longer precompiling it; but on-demand compilation triggered by the categories library fails because of missing write permissions.

And after all that effort we went to have graceful deprecation of modules 😢 Sounds like we shouldn't remove the deprecated modules from Everything.agda?

And after all that effort we went to have graceful deprecation of modules cry Sounds like we shouldn't remove the deprecated modules from Everything.agda?

This would keep stuff working but the reality is that every downstream library needs a new release every time standard library updates as things shouldn't really be using deprecated modules

@MatthewDaggitt It's great that you put effort into graceful deprecation. The real problem is that Agda has no clear concept of what a package consists of, so we just build everything in Everything.agda, and nothing else. If people would make a local copy of agda-stdlib, they could still use the deprecated module, it would then be built when it's used. But nixpkgs tries to be "cleaner" than that and fail if anyone uses a deprecated module.

Just to add to this, this is caused by nix packages being immutable once built, so if something doesn't get compiled when we build the package then it is unusable

I didn't know about our policy of always having a working Agda library set

It's not really set in stone, we're all in the process of figuring this out. My aim is that nixpkgs plays a similar role for Agda like stackage does for Haskell.

I'll try to look into the upstream issues!

That definitely a good idea. Often, a short PR is all it needs.

@turion I added v0.2 tag for the functional-linear-algebra package that should work with agda stdlib 1.5. Should I make a PR on top of this one to add that new commit?

@ryanorendorff Thanks a lot :) if it's a simple version bump then it's probably easiest if @iblech adds one commit to this PR here. If it's more, e.g. changed dependencies or build process, then it is probably helpful to make a PR onto the iblech:patch-agdastdlib15 branch.

I'll quickly add the version bump to this pull request, and I have also given you two (turion and ryanorendorff) write access to my fork. Feel free to commit as you wish there. :-)

Do all libraries build now? See #98209 (comment)

Huh. For some reason, ofborg builds some libraries. Not sure what's going on there.

Yes, they do! :-)

$ nix-shell -I nixpkgs=https://github.com/iblech/nixpkgs/archive/patch-agdastdlib15.tar.gz -p 'agda.withPackages (lib.attrValues (lib.filterAttrs (name: value: (builtins.isAttrs value && builtins.hasAttr "isAgdaDerivation" value && value.isAgdaDerivation && !value.meta.broken)) agdaPackages))'
unpacking 'https://github.com/iblech/nixpkgs/archive/patch-agdastdlib15.tar.gz'...
[nix-shell:~] $

Edit: In other words, I believe this pull request is now fit for merging.

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

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

Awesome @AndersonTorres, thank you very much for the quick merge! :-) I really like that we have such a fast turnaround time. Thanks also to all the other involved persons!

Yes, updating the agda standard library is a surprisingly pleasant process :)