Build the Conway spec in CI

IntersectMBO · May 7, 2024 · 8254ae8 · 8254ae8
1 parent d9a802f
commit 8254ae8
Show file tree

Hide file tree

Showing 5 changed files with 30 additions and 5 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - uses: cachix/install-nix-action@v20
         with:
@@ -45,14 +45,14 @@ jobs:
 
       - name: Upload PDF artifacts
         if: github.event_name == 'pull_request'
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: PDF specs
           path: docs/pdfs/*.pdf
 
       - name: Upload typechecking times
         if: github.event_name == 'pull_request'
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: Typechecking durations
           path: docs/*.time

diff --git a/README.md b/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.

diff --git a/default.nix b/default.nix
@@ -170,13 +170,33 @@ rec {
     #   dontInstall = true;
     # };
 
-    hsExe = haskellPackages.callCabal2nix "${project}" "${hsSrc}/haskell/${main}" { };
+    hsExe = haskellPackages.callCabal2nixWithOptions "${project}" "${hsSrc}/haskell/${main}" "--no-haddock" {};
 
   };
 
+  mkPdfDerivation = name: version: project: stdenv.mkDerivation {
+    inherit (locales) LANG LC_ALL LOCALE_ARCHIVE;
+    pname = name;
+    version = version;
+    src = "${formalLedger}";
+    meta = { };
+    buildInputs = [ agdaWithDeps latex ];
+    buildPhase = ''
+        mkdir -p latex/Ledger
+        OUT_DIR=$out make ${project}
+      '';
+    doCheck = true;
+    checkPhase = ''
+        test -n "$(find $out/pdfs/ -type f -name '*.pdf')"
+      '';
+    dontInstall = true;
+  };
+
   ledger = mkSpecDerivation {
     project = "ledger";
     main = "Ledger";
+  } // {
+    conway = mkPdfDerivation "conway-formal-spec" "0.9" "ledger.conway.docs";
   };
   midnight = mkSpecDerivation {
     project = "midnight";

diff --git a/src/Ledger/Introduction.lagda b/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}

diff --git a/src/latex/agda-latex-macros.sty b/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}