Skip to content

Build executable Agda spec via haskell.nix instead of the Nixpkgs haskell infraย #1697

@amesgen

Description

@amesgen

Re #1586 (comment)

  • The Agda spec for header validation is executable, and we use Agda's Haskell backend to generate Haskell source code that we can use (eventually for proper conformance tests).
  • Currently, we use the Nixpkgs Haskell infrastructure to build that generated code (I think this is mostly because the Ledger spec does this, and we inherited it from there.)
  • However, Use the real crypto in formal spec testsย #1586 starts to depend on CHaP for that code, and the Nixpkgs Haskell infra doesn't support custom repositories. So we should switch it to haskell.nix (which we already use for building our "main" code).

(Eventually, we might want to integrate it into our "main" project, but that requires some decisions such as whether we want to check in the generated code.)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    Status

    ๐Ÿ”– Ready

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions