IntersectMBO / IntersectMBO/ouroboros-consensus

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

Open
#1,697 0 comments 0 reactions 0 assignees View on GitHub
continuous integration
Dominant language
Haskell
Stars
67
Forks
43
Avg merge
5d 13h
Merged PRs (30d)
43

Description

Re https://github.com/IntersectMBO/ouroboros-consensus/pull/1586#issuecomment-3200962406

- 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](https://github.com/IntersectMBO/ouroboros-consensus/blob/ac1a8db76f4c7a38a9a6b962a40fa722d5bd55a6/nix/agda.nix#L108) to build that generated code (I think this is mostly because the Ledger spec does this, and we inherited it from there.)
- However, https://github.com/IntersectMBO/ouroboros-consensus/pull/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.)

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.