Build the Conway spec in CI

README.md

@@ -6,7 +6,8 @@ This repository currently contains two specifications---the work in progress spe
 
 Formal Specification | HTML Version | Haskell Tests |
 ----------------------|--------------|---------------|
-[Cardano Ledger](https://IntersectMBO.github.io/formal-ledger-specifications/pdfs/cardano-ledger.pdf) | [Ledger.PDF](https://IntersectMBO.github.io/formal-ledger-specifications/html/Ledger.PDF.html) | [UTXOW test](https://IntersectMBO.github.io/formal-ledger-specifications/haskell/Ledger/test/UtxowSpec.hs) |
+[Full Cardano Ledger](https://IntersectMBO.github.io/formal-ledger-specifications/pdfs/cardano-ledger.pdf) | [Ledger.PDF](https://IntersectMBO.github.io/formal-ledger-specifications/html/Ledger.PDF.html) | [UTXOW test](https://IntersectMBO.github.io/formal-ledger-specifications/haskell/Ledger/test/UtxowSpec.hs) |
+[Conway](https://IntersectMBO.github.io/formal-ledger-specifications/pdfs/conway-ledger.pdf) | [Ledger.PDF](https://IntersectMBO.github.io/formal-ledger-specifications/html/Ledger.PDF.html) | [UTXOW test](https://IntersectMBO.github.io/formal-ledger-specifications/haskell/Ledger/test/UtxowSpec.hs) |
 [Midnight Example](https://IntersectMBO.github.io/formal-ledger-specifications/pdfs/midnight-example.pdf) | [MidnightExample.PDF](https://IntersectMBO.github.io/formal-ledger-specifications/html/MidnightExample.PDF.html) | [LEDGER test](https://IntersectMBO.github.io/formal-ledger-specifications/haskell/MidnightExample/test/LedgerSpec.hs) |
 
 Note: the HTML versions of the specifications are interactive, but many modules currently contain LaTeX code which is used to generate the PDF. We intend to fix this eventually.

default.nix

@@ -177,6 +177,24 @@ rec {
   ledger = mkSpecDerivation {
     project = "ledger";
     main = "Ledger";
+  } // {
+    conway = stdenv.mkDerivation {
+      inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
+      pname = "docs";
+      version = "0.1";
+      src = "${formalLedger}";
+      meta = { };
+      buildInputs = [ agdaWithDeps latex ];
+      buildPhase = ''
+        OUT_DIR=$out make ledger.conway.docs
+      '';
+      doCheck = true;
+      checkPhase = ''
+        test -n "$(find $out/pdfs/ -type f -name '*.pdf')"
+      '';
+      dontInstall = true;
+    };
+
   };
   midnight = mkSpecDerivation {
     project = "midnight";

src/Ledger/Introduction.lagda

@@ -26,6 +26,9 @@ with previous specifications, this document is an incremental
 specification, so everything that isn't defined here refers to the
 most recent definition from an older specification.
 
+Note: As of now, this specification is still a draft. Some details and
+explanations may be missing or wrong.
+
 \end{Conway}
 
 \begin{NoConway}

src/latex/agda-latex-macros.sty

@@ -384,6 +384,7 @@
 \newcommand{\Pthree}{\AgdaField{P3}\xspace}
 \newcommand{\Ptwoa}{\AgdaField{P2a}\xspace}
 \newcommand{\Ptwob}{\AgdaField{P2b}\xspace}
+\newcommand{\Pfive}{\AgdaField{P5}\xspace}
 \newcommand{\pv}{\AgdaField{pv}\xspace}
 
 \newcommand{\Qone}{\AgdaField{Q1}\xspace}