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

agda2hs fails unless agda or agda2hs is run first #322

Open
bwbush opened this issue May 9, 2024 · 2 comments
Open

agda2hs fails unless agda or agda2hs is run first #322

bwbush opened this issue May 9, 2024 · 2 comments
Labels
bug Something isn't working

Comments

@bwbush
Copy link

bwbush commented May 9, 2024

The first execution of agda2hs fails for this code:

$ find -type f -name \*.agdai -delete

$ agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda

agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda
Checking Peras.QCD.Node.Specification (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Specification.agda).
 Checking Peras.QCD.Crypto (/extra/iohk/peras-design.msd/src/Peras/QCD/Crypto.agda).
 Checking Peras.QCD.Crypto.Placeholders (/extra/iohk/peras-design.msd/src/Peras/QCD/Crypto/Placeholders.agda).
  Checking Peras.QCD.Types (/extra/iohk/peras-design.msd/src/Peras/QCD/Types.agda).
   Checking Peras.QCD.Protocol (/extra/iohk/peras-design.msd/src/Peras/QCD/Protocol.agda).
  Checking Peras.QCD.Types.Instances (/extra/iohk/peras-design.msd/src/Peras/QCD/Types/Instances.agda).
   Checking Peras.QCD.Util (/extra/iohk/peras-design.msd/src/Peras/QCD/Util.agda).
 Checking Peras.QCD.Node.Model (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Model.agda).
  Checking Peras.QCD.State (/extra/iohk/peras-design.msd/src/Peras/QCD/State.agda).
 Checking Peras.QCD.Node.Preagreement (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Preagreement.agda).
/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Specification.agda:233,29-235,93
illegal instance:  iHashEq

$ agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda

Success also occurs if agda is run and then agda2hs is run:

$ find -type f -name \*.agdai -delete

$ agda --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda

Checking Peras.QCD.Node.Specification (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Specification.agda).
 Checking Peras.QCD.Crypto (/extra/iohk/peras-design.msd/src/Peras/QCD/Crypto.agda).
 Checking Peras.QCD.Crypto.Placeholders (/extra/iohk/peras-design.msd/src/Peras/QCD/Crypto/Placeholders.agda).
  Checking Peras.QCD.Types (/extra/iohk/peras-design.msd/src/Peras/QCD/Types.agda).
   Checking Peras.QCD.Protocol (/extra/iohk/peras-design.msd/src/Peras/QCD/Protocol.agda).
  Checking Peras.QCD.Types.Instances (/extra/iohk/peras-design.msd/src/Peras/QCD/Types/Instances.agda).
   Checking Peras.QCD.Util (/extra/iohk/peras-design.msd/src/Peras/QCD/Util.agda).
 Checking Peras.QCD.Node.Model (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Model.agda).
  Checking Peras.QCD.State (/extra/iohk/peras-design.msd/src/Peras/QCD/State.agda).
 Checking Peras.QCD.Node.Preagreement (/extra/iohk/peras-design.msd/src/Peras/QCD/Node/Preagreement.agda).

$ agda2hs --local-interfaces --library-file=$AGDA_LIBS --compile-dir=peras-hs/src src/Peras/QCD/Node/Specification.agda
@jespercockx jespercockx added the bug Something isn't working label May 24, 2024
@jespercockx
Copy link
Member

This sounds like an upstream issue in Agda rather than a bug in agda2hs itself. Perhaps it could be fixed by agda/agda#7251?

@jespercockx
Copy link
Member

@bwbush Could you provide a minimized reproducer for this issue? Otherwise it is not really possible to look deeper into it.

Alternatively, you could try to use a patched version of agda2hs that includes the patch to base agda I mentioned above.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants