You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I am not using nix (and don't plan to), and am having trouble to load the library in agda.
I fixed ~/.agda/libraries to use the versions referenced in the default.nix file which got me quite far, except that I am now hitting this issue:
———— Error —————————————————————————————————————————————————
~/formal-ledger-specifications/src/Data/List/Ext/Properties.agda:203,60-74
The constructor Algebra.Definitions.RawMagma._,_ does not construct
an element of Σ
when checking that the expression <″-offset refl has type
y ∷ [] ≡ [] ++ [ y ] ++ [] × [] ≡ [] ++ []
This might come from a wrong stdlib but while the nix file references a v2.0-rc1 version, I could not find this version in the agda-stdlib source tree.
Would it be possible to provide instructions to build the library without nix? I would be happy to do that but I would need to fix my own setup first hence the need for some guidance of what are the right versions.
The text was updated successfully, but these errors were encountered:
Looks like the stdlib has changed something since the RC. We switched to that really early since we were relying on a custom patched one before and didn't bother updating things since then. We've also not updated Agda since 2.6.4.
I am not using nix (and don't plan to), and am having trouble to load the library in agda.
I fixed
~/.agda/libraries
to use the versions referenced in thedefault.nix
file which got me quite far, except that I am now hitting this issue:This might come from a wrong stdlib but while the nix file references a
v2.0-rc1
version, I could not find this version in the agda-stdlib source tree.Would it be possible to provide instructions to build the library without nix? I would be happy to do that but I would need to fix my own setup first hence the need for some guidance of what are the right versions.
The text was updated successfully, but these errors were encountered: