Formal and executable specifications for the bcc chain

This directory is organized as follows:

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

Building the documents

To build the LaTeX document run:

nix-shell --pure --run make

For a continuous compilation of the LaTeX file run:

nix-shell --pure --run "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 start a REPL first make sure to run the configure script:

nix-shell --pure --run "runhaskell Setup.hs configure"

then run:

nix-shell --pure --run "runhaskell Setup.hs repl"

To test run:

nix-shell --pure --run "runhaskell Setup.hs test"

Development

For running the tests you can use:

nix-shell --pure --command "cabal new-test <target>"

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

nix-shell --pure --run "cabal new-test ledger-delegation-test"

To have the warnings not being treated as errors the development flag can be used, e.g.:

nix-shell --pure --run "cabal new-test ledger-delegation-test -fdevelopment"