Everything.agda does not build (with standard library 1.7.1?)

[turion]

Occurred during NixOS/nixpkgs#153757. Build failure:

Checking Everything (/build/source/Everything.agda).
 Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda).
 Checking Generics.Telescope (/build/source/src/Generics/Telescope.agda).
 Checking Generics.Telescope.Equality (/build/source/src/Generics/Telescope/Equality.agda).
/build/source/src/Generics/Telescope/Equality.agda:26,13-14
Not in scope:
  J at /build/source/src/Generics/Telescope/Equality.agda:26,13-14
when scope checking J

[turion]

This problem persists even in version 1.0.0:

Checking Everything (/build/source/Everything.agda).
 Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda).
 Checking Generics.Telescope (/build/source/src/Generics/Telescope.agda).
 Checking Generics.Telescope.Equality (/build/source/src/Generics/Telescope/Equality.agda).
/build/source/src/Generics/Telescope/Equality.agda:26,13-14
Not in scope:
  J at /build/source/src/Generics/Telescope/Equality.agda:26,13-14
when scope checking J

See NixOS/nixpkgs#153757

[flupe]

Yes sorry about that, I've developed this library while relying on the development version of the stdlib.
I've been waiting for the stdlib to get a new release (where J is defined) but don't know when this will happen. Maybe it would be best to re-implement J on my end, even if it gets removed later on.

[flupe]

Do you keep track of which version of the stdlib this library depends on when you package it for nix ?

[turion]

It is possible in principle to do that in nixpkgs, although we haven't done it in agdaPackages yet because it means extra maintenance effort. Our goal is to have a coherent package set where every package is compatible with every other one.

Maybe it would be best to re-implement J on my end, even if it gets removed later on.

That sounds like a good plan. If it's ok for you copying the J code into your repo temporarily and pin the standard library version to 1.7.1 until the next release, that's the better solution :) And you'll get a free ping when your package doesn't work anymore with the newest standard library.

[turion]

#11