Improve building the PDF via Makefile

CONTRIBUTING.md

@@ -40,6 +40,14 @@ To install Agda locally and use that install with emacs, you can do the followin
 
 `nix-shell` provides Agda complete with the correct dependencies. So you should be able to run your preferred editor within `nix-shell` and it should see the required `agda` executable.
 
+## Building the PDF quickly
+
+The Makefile can be used to build the PDF without having to build everything else. Either run `make` from within `nix-shell`, or use
+```
+nix-shell --command make
+```
+to run `make` without launching an interactive shell.
+
 ## Updating nixpkgs
 
 To update the default nixpkgs used to build the derivations, run

Makefile

@@ -1,13 +1,13 @@
-tex_files := Introduction.tex BaseTypes.tex TokenAlgebra.tex Crypto.tex Address.tex Script.tex GovernanceActions.tex PParams.tex Transaction.tex Utxo.tex Utxow.tex Tally.tex Deleg.tex Ledger.tex Ratify.tex Chain.tex Utxo/Properties.tex PDF.tex
+tex_files := Introduction.tex BaseTypes.tex TokenAlgebra.tex Crypto.tex Address.tex Script.tex GovernanceActions.tex PParams.tex Transaction.tex Utxo.tex Utxow.tex Gov.tex Deleg.tex Ledger.tex Ratify.tex Chain.tex Utxo/Properties.tex PDF.tex
 
 tex_files2 := $(addprefix src/latex/Ledger/, $(tex_files))
 
 .PHONY: all clean
 src/latex/Ledger/%.tex: src/Ledger/%.lagda
 	cd src && agda --only-scope-checking --latex ../$<
 all: $(tex_files2)
-	cd src/latex && xelatex Ledger/PDF.tex
-	cp src/latex/PDF.pdf .
+	cd src/latex && latexmk -xelatex Ledger/PDF.tex
+	cp src/latex/PDF.pdf cardano-ledger.pdf
 clean:
 	rm -rf src/latex
 	rm -rf src/MAlonzo

README.md

@@ -39,7 +39,7 @@ nix-build -A midnight.docs             # build the Midnight example docs
 The `executableSpec` is a `cabal` package, which can be loaded into GHCI like this:
 
 ```
-nix-shell --command "cabal repl --build-depends 'agda-ledger-executable-spec, agda-ledger-executable-spec-midnight'"
+nix-shell -A run --command "cabal repl --build-depends 'agda-ledger-executable-spec, agda-ledger-executable-spec-midnight'"
 λ> :m HSLedgerTest
 λ> main
 ```

shell.nix

@@ -9,13 +9,21 @@ with pkgs;
 
 let specs = callPackage ./default.nix {};
 
-in mkShell {
-  nativeBuildInputs = [
-    specs.agda
-    cabal-install
-    (haskellPackages.ghcWithPackages (pkgs: with pkgs; [
-      specs.ledger.executableSpec
-      specs.midnight.executableSpec
-    ]))
-  ];
+in {
+  shell = mkShell {
+    nativeBuildInputs = [
+      specs.agdaWithStdLibMeta
+    ];
+  };
+
+  run.shell = mkShell {
+    nativeBuildInputs = [
+      specs.agda
+      cabal-install
+      (haskellPackages.ghcWithPackages (pkgs: with pkgs; [
+        specs.ledger.executableSpec
+        specs.midnight.executableSpec
+      ]))
+    ];
+  };
 }