Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nix-less instructions to build the library #431

Open
abailly opened this issue May 25, 2024 · 3 comments
Open

Nix-less instructions to build the library #431

abailly opened this issue May 25, 2024 · 3 comments

Comments

@abailly
Copy link

abailly commented May 25, 2024

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.

@abailly
Copy link
Author

abailly commented May 25, 2024

% agda --version
Agda version 2.6.4.3
Built with flags (cabal -f)
 - optimise-heavily: extra optimisations 

@WhatisRT
Copy link
Collaborator

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.

@WhatisRT
Copy link
Collaborator

The issue you've found is fixed in #432. Nix-less instructions would be very welcome!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants