search

flupe / generics

MIT License
21 stars 6 forks source link

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

Closed turion closed 4 days ago

turion commented 2 years ago

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
turion commented 2 years ago

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

flupe commented 2 years ago

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 commented 2 years ago

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

turion commented 2 years ago

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 commented 4 days ago

https://github.com/flupe/generics/issues/11