byron

Formal and executable specifications for the cardano chain

This directory is organized as follows:

• ledger/formal-spec contains the LaTeX specification of Cardano ledger semantics.
• ledger/executable-spec contains an executable specification of Cardano ledger semantics.
• chain/formal-spec contains the LaTeX specification of Cardano chain semantics.
• chain/executable-spec contains an executable specification of Cardano chain semantics.

Building the documents

To build the LaTeX document run:

nix develop --command make

For a continuous compilation of the LaTeX file run:

nix develop --command make watch

Building the executable specification

The executable specifications can be built and tested using Nix.

To build to go to the directory in which the executable specifications are (e.g. ledger/executable-spec) and then run:

nix build

To build, or run, tests:

nix build .#tests
nix run .#tests

Development

For running the tests you can use, in a nix develop shell:

cabal new-test <target>

Example, while in the byron/ledger/executable-spec directory one can run:

cabal new-test ledger-delegation-test

To have the warnings not being treated as errors the -Wwarn ghc flag can be used to negate the effect of -Werror, e.g.:

cabal new-test ledger-delegation-test --ghc-options='-Wwarn'