Repository navigation
Support Agda 2.6.2 & standard-library 1.7 #9
Description
Currently there is a build failure like:
Checking Everything (/build/source/Everything.agda).
Checking Generic.Test (/build/source/src/Generic/Test.agda).
Checking Generic.Test.Data (/build/source/src/Generic/Test/Data.agda).
Checking Generic.Test.Data.Fin (/build/source/src/Generic/Test/Data/Fin.agda).
Checking Generic.Main (/build/source/src/Generic/Main.agda).
Checking Generic.Core (/build/source/src/Generic/Core.agda).
Checking Generic.Lib.Prelude (/build/source/src/Generic/Lib/Prelude.agda).
Checking Generic.Lib.Intro (/build/source/src/Generic/Lib/Intro.agda).
Checking Generic.Lib.Equality.Propositional (/build/source/src/Generic/Lib/Equality/Propositional.agda).
Checking Generic.Lib.Equality.Coerce (/build/source/src/Generic/Lib/Equality/Coerce.agda).
Checking Generic.Lib.Decidable (/build/source/src/Generic/Lib/Decidable.agda).
Checking Generic.Lib.Equality.Heteroindexed (/build/source/src/Generic/Lib/Equality/Heteroindexed.agda).
Checking Generic.Lib.Data.Sum (/build/source/src/Generic/Lib/Data/Sum.agda).
Checking Generic.Lib.Data.Product (/build/source/src/Generic/Lib/Data/Product.agda).
Checking Generic.Lib.Category (/build/source/src/Generic/Lib/Category.agda).
Checking Generic.Lib.Equality.Congn (/build/source/src/Generic/Lib/Equality/Congn.agda).
Checking Generic.Lib.Data.Nat (/build/source/src/Generic/Lib/Data/Nat.agda).
Checking Generic.Lib.Data.Pow (/build/source/src/Generic/Lib/Data/Pow.agda).
Checking Generic.Lib.Data.Sets (/build/source/src/Generic/Lib/Data/Sets.agda).
Checking Generic.Lib.Data.String (/build/source/src/Generic/Lib/Data/String.agda).
Checking Generic.Lib.Data.Maybe (/build/source/src/Generic/Lib/Data/Maybe.agda).
Checking Generic.Lib.Data.List (/build/source/src/Generic/Lib/Data/List.agda).
Checking Generic.Lib.Reflection.Core (/build/source/src/Generic/Lib/Reflection/Core.agda).
/build/source/src/Generic/Lib/Reflection/Core.agda:8,45-90
The module Reflection.Argument.Information doesn't export the
following:
relevance
when scope checking the declaration
open import Reflection.Argument.Information public
using (ArgInfo; visibility; relevance)
/build/source/src/Generic/Lib/Reflection/Core.agda:174,37-46
Not in scope:
relevance
at /build/source/src/Generic/Lib/Reflection/Core.agda:174,37-46
(did you mean
'Agda.Builtin.Reflection.Relevance.relevant' or
'Agda.Builtin.Reflection.Relevance' or
'Agda.Builtin.Reflection.relevant' or
'Reflection._
See:
Activity
isovector commentedon Dec 6, 2021
I'd like this too!
effectfully commentedon Dec 7, 2021
I'll look into it this weekend.
effectfully commentedon Dec 14, 2021
(my machine has died, so the next weekend or the one after that)
effectfully commentedon Jan 4, 2022
So I tried to update the library, but
Reflectionhas changed a lot and now it's not clear to me at all how to do the same thing that I used to do before with the new version ofReflection. In particular, in some placesStringnames have changed to De Bruijn indices and it's not clear to me how to move from the latter to the former (or vice versa).I have like zero time these days, so that's about as much as I can contribute.
You will likely have better luck with https://github.com/flupe/generics
isovector commentedon Jan 4, 2022
Thanks for investigating, and for all of your time!