search

IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger
Apache License 2.0
32 stars 13 forks source link

Nix-less instructions to build the library #431

Open abailly opened 1 month ago

abailly commented 1 month ago

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 commented 1 month ago 
% agda --version
Agda version 2.6.4.3
Built with flags (cabal -f)
 - optimise-heavily: extra optimisations
WhatisRT commented 1 month ago

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 commented 1 month ago

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