flupe
Everything.agda does not build (with standard library 1.7.1?)
Occurred during https://github.com/NixOS/nixpkgs/pull/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
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 https://github.com/NixOS/nixpkgs/pull/153757
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.
Do you keep track of which version of the stdlib this library depends on when you package it for nix ?
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
Jon 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.