Currently rebased onto #98199 to get a feeling whether this is feasible.

I'm not sure this achieves what you want in that I don't think these tests will be ran by ofBorg when you update standard-library

Yes, true :/ Do you have an idea how to go about this?

Disclaimer that I am not sure about this but this is what I believe happens:

• When you submit the PR, by default ofBorg just checks that the nix evaluates (i.e. doesn't build anything)
• If the user is recognised(?) by ofBorg (via putting in a pr to ofBorg) and the pr title has a certain format, or if someone types ofBorg build (but actually tagging ofBorg), it tries to build the package and runs any tests contained in passthru.tests

However the CI checks have looked a bit different recently, and I'm not sure if there is a detailed description of what they do somewhere

@alexarice Does that mean this is still useful? Maybe one of us can get ofBorg rights to trigger the build.

I have ofBorg rights, that is not the problem. The problem is that as I understand it you want:
PR put in for standard library -> ofBorg tests all downstream packages.

The test you have added does not do this. It adds checking all agda packages to the agda test, which can only be run manually.

Right now it's fine for me if the packages are built either automatically or by triggering ofBorg manually. These PRs are still rare enough that we'll always notice. I'm fine with going with the solution that is most likely to be merged.

I could even imagine an allPackages derivation that simply has all agda packages as build inputs and does nothing otherwise, and when reviewing one can simply build that locally to verify that nothing was broken.

Maybe there is a standard way to check for breakages in downstream packages?

I just don't feel this test is checking if the agda infrastructure is broken which shouldn't be the case if one leaf package is a bit dodgy

Maybe there is a standard way to check for breakages in downstream packages?

How is it done in Haskell?

They update the whole package set with cabal2nix at one time and then I guess build the whole thing manually and see what packages broke though I am not an expert

Ok, we can't quite copy that workflow yet (see #87903 though for an initial idea how to do that). How about the easiest way, just make a set allUnbrokenPackages, document it, and we can remind people on PRs to build it locally in order to ensure that there are no breakages?

Does anything else do this?

Does anything else do this?

I don't know, I'm not really involved in any other language frameworks.

I'm not really against it, just seems odd to have a meta-package in the package set, really feels like it should be a test

Understandable.

So a separate test? In nixos/tests/agda/allUnbrokenPackages.nix? How would it look like? It wouldn't do anything in the body, it just has all unbroken packages as dependencies?

I'm afraid I don't really know enough about testing

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

https://discourse.nixos.org/t/how-to-test-all-agda-packages/9545/1

@ofborg build agdaPackages.standard-library.passthru.tests

@alexarice @neosimsim what do you think about this? I'd like to merge this before the next standard library is released (in the next days), so we can test the workflow.

I'm not sure about all the changes to the documentation, as I believe that is aimed more at users, but I am happy with all the code changes

I'm not sure about all the changes to the documentation, as I believe that is aimed more at users, but I am happy with all the code changes

Yes, I understand. That's why this section is at the end, so mere users will stop reading at some point and not miss anything important. However my impression is that nixpkgs is a rabbit hole, and after some time of using, users automatically evolve into maintainers, and then it's great if they have some docs to get started. (I remember having a hard time starting to contribute to the Haskell ecosystem in nixpkgs, and I'd like to prevent that for future maintainers.) Also, sometimes Agda library authors might want to have their library included, so they can directly jump to that place.

Should I maybe add a sentence saying something to the effect of "If you just want to use Agda, you don't need to read this"?

I'm not sure about all the changes to the documentation, as I believe that is aimed more at users

For example python also has a section about how python is packaged in nixpkgs. So I think it's fine to have a separate section on that.

@ofborg build agdaPackages.standard-library.passthru.tests
@ofborg build agdaPackages.passthru.tests

@ofborg build agda.passthru.tests.all

@alexarice @neosimsim Comments? Otherwise I'm going to go find someone to merge ;)

@ofborg build agdaPackages.standard-library.passthru.tests
@ofborg build agdaPackages.passthru.tests.allPackages

@ofborg build agda.passthru.tests.allPackages

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

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