Makefile: also generate HTML + Haskell code

- More modular haskell project structure:
  + A single `Lib.hs` file now re-exports all (exposed) modules.
  + A single `Main.hs` acts as the entry-point for running the project.

- the Makefile is still not entirely polished and will be improved later
  + e.g. too much duplication of similar commands

.gitignore

@@ -7,3 +7,6 @@ result*
 *.pdf
 src/latex/Ledger/*
 src/latex/MidnightExample/*
+src/latex/bclogo.sty
+
+dist/

CONTRIBUTING.md

@@ -14,6 +14,8 @@ To install Agda locally and use that install with emacs, you can do the followin
 
    *Note*. You need not have built/installed Agda prior to invoking this `nix-build` command (though it's okay if you have).
 
+   *Note*. To instruct the `Makefile` to use this local Agda binary, invoke it like so: `AGDA=~/IOHK/ledger-agda make -C src/`
+
 -  Put the following into your init file (highlight and `M-x eval-region` to load it without restarting emacs).
 
    ```
@@ -44,10 +46,20 @@ To install Agda locally and use that install with emacs, you can do the followin
 
 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
+nix-shell --command 'make docs'
 ```
 to run `make` without launching an interactive shell.
 
+This combines well with the ability to invoke the TeX backend of Agda within Emacs,
+which is much faster when you have already loaded an Agda file/interface.
+
+## Building other artifacts
+
+Apart from the PDF specification, the `Makefile` can be used to also generate the following:
+- `make html`: generate HTML under `dist/html/`
+- `make codeGen`: generate Haskell code under `dist/MAlonzo/`
+- `make hsBuild`: run the Haskell test of each Agda formmalisation
+
 ## Updating nixpkgs
 
 To update the default nixpkgs used to build the derivations, run

Makefile

@@ -0,0 +1,12 @@
+.PHONY: all docs html codeGen hsBuild
+
+all:
+	$(MAKE) -C src/
+docs:
+	$(MAKE) -C src/ docs
+html:
+	$(MAKE) -C src/ html
+codeGen:
+	$(MAKE) -C src/ codeGen
+hsBuild:
+	$(MAKE) -C src/ hsBuild

default.nix

@@ -68,7 +68,7 @@ rec {
   };
 
   # a parameterized attribute set containing derivations for: 1) executable spec 2) docs
-  specsDerivations = { dir, agdaLedgerFile, hsMainFile, doc }:
+  specsDerivations = { dir, agdaLedgerFile, project }:
     let
       hsSrc =
         stdenv.mkDerivation {
@@ -80,11 +80,11 @@ rec {
           buildPhase = "";
           installPhase = ''
             mkdir -p $out
+            cp ${dir}/*.hs $out
+            cp ${dir}/*.cabal $out
             agda -c --ghc-dont-call-ghc --compile-dir $out ${dir}/${agdaLedgerFile}
-            cp ${dir}/${hsMainFile} $out
-            cp ${dir}/agda-ledger-executable-spec.cabal $out
             # Append all the modules generated by MAlonzo to the cabal file
-            find $out/MAlonzo -name "*.hs" -print | sed "s#^$out/#        #;s#\.hs##;s#/#.#g" >> $out/agda-ledger-executable-spec.cabal
+            find $out/MAlonzo -name "*.hs" -print | sed "s#^$out/#        #;s#\.hs##;s#/#.#g" >> $out/${project}.cabal
           '';
         };
       docs = stdenv.mkDerivation {
@@ -100,7 +100,7 @@ rec {
         installPhase = ''
           mkdir -p $out
           agda --html --html-dir $out/html ${dir}/PDF.lagda
-          cp latex/PDF.pdf $out/${doc}.pdf
+          cp latex/PDF.pdf $out/${project}.pdf
         '';
       };
     in
@@ -112,15 +112,13 @@ rec {
     };
 
   ledger = specsDerivations {
+    project = "cardano-ledger";
     dir = "Ledger";
     agdaLedgerFile = "Foreign/HSLedger.agda";
-    hsMainFile = "HSLedgerTest.hs";
-    doc = "cardano-ledger";
   };
   midnight = specsDerivations {
+    project = "midnight-example";
     dir = "MidnightExample";
     agdaLedgerFile = "HSLedger.agda";
-    hsMainFile = "Main.hs";
-    doc = "midnight-example";
   };
 }

src/Ledger/Foreign/LedgerTypes.agda

@@ -32,7 +32,6 @@ TxId          = ℕ
 Ix            = ℕ
 Epoch         = ℕ
 AuxiliaryData = ⊤
-Network       = ⊤
 
 TxIn          = Pair TxId Ix
 TxOut         = Pair Addr Coin

src/Ledger/Lib.hs

@@ -0,0 +1,8 @@
+module Lib
+  ( module MAlonzo.Code.Ledger.Foreign.LedgerTypes
+  , module MAlonzo.Code.Ledger.Foreign.HSLedger
+  ) where
+
+import MAlonzo.Code.Ledger.Foreign.LedgerTypes
+import MAlonzo.Code.Ledger.Foreign.HSLedger
+

src/Ledger/HSLedgerTest.hs → src/Ledger/Main.hs

@@ -1,7 +1,6 @@
-module HSLedgerTest (module HSLedgerTest, module MAlonzo.Code.Ledger.Foreign.LedgerTypes, module MAlonzo.Code.Ledger.Foreign.HSLedger) where
+module Main where
 
-import MAlonzo.Code.Ledger.Foreign.HSLedger
-import MAlonzo.Code.Ledger.Foreign.LedgerTypes
+import Lib
 
 initParams :: PParams
 initParams = MkPParams

src/Ledger/agda-ledger-executable-spec.cabal → src/Ledger/cardano-ledger.cabal

@@ -1,5 +1,5 @@
 cabal-version:      2.4
-name:               agda-ledger-executable-spec
+name:               cardano-ledger
 version:            0.1.0.0
 synopsis:
 
@@ -18,23 +18,31 @@ maintainer:         [email protected]
 -- category:
 extra-source-files: CHANGELOG.md
 
+executable main
+    main-is: Main.hs
+    ghc-options: -Wno-missing-home-modules
+    build-depends:
+        base,
+        text,
+        ieee,
+        tree-diff,
+        cardano-ledger
+
 library
     exposed-modules:
-        HSLedgerTest
-
-    other-extensions:
-        CPP PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
-        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
-        PatternSynonyms DeriveGeneric
-
+        Lib
     build-depends:
         base,
         text,
         ieee,
         tree-diff
-
-    ghc-options: -Wno-overlapping-patterns
-    hs-source-dirs:   .
+    hs-source-dirs: .
     default-language: Haskell2010
+    ghc-options:
+        -Wno-overlapping-patterns
+    other-extensions:
+        CPP PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
+        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
+        PatternSynonyms DeriveGeneric
 -- This will be generated automatically when building with nix
     other-modules:

src/Makefile

@@ -1,40 +1,83 @@
-LATEX=latexmk -xelatex -shell-escape -halt-on-error
+# Constants
+AGDA?=agda
+OUT_DIR?=../dist
+LATEX?=latexmk -xelatex -shell-escape -halt-on-error
 LATEX_DIR=latex
 PRE=$(addprefix $(LATEX_DIR)/, \
   agda.sty agda-latex-macros.sty iohk.sty fonts/* preamble.tex)
-AGDA=/home/omelkonian/IOHK/agdaWithStdLibMeta/bin/agda \
-  --latex --latex-dir=$(LATEX_DIR) # --only-scope-checking
+HTML_DIR=$(OUT_DIR)/html
+HS_DIR=$(OUT_DIR)/MAlonzo
+HS_DIR_LEDGER=$(HS_DIR)/Ledger
+HS_DIR_MIDNIGHT=$(HS_DIR)/MidnightExample
 
-.PHONY: default clean all
+.PHONY: default clean all docs html codeGen hsBuild
 default: all
 
-all: $(latexFiles)
-
-# Compile a literate Agda file to LaTeX.
+# Agda -> LaTeX -> PDF
 latexFiles=$(patsubst %.lagda, $(LATEX_DIR)/%.tex, \
              $(shell find . -name '*.lagda' | sed 's|\.\/||g'))
 $(latexFiles): $(LATEX_DIR)/%.tex: %.lagda
 	@echo "Compiling $<"
-	$(AGDA) $<
+	$(AGDA) --latex --latex-dir=$(LATEX_DIR) $< # --only-scope-checking
 
-../cardano-ledger.pdf: $(LATEX_DIR)/Ledger/PDF.tex $(latexFiles) $(PRE)
+$(OUT_DIR)/cardano-ledger.pdf: $(LATEX_DIR)/Ledger/PDF.tex $(latexFiles) $(PRE)
 	@echo "Generating $@"
 	cd $(LATEX_DIR) && $(LATEX) $(subst $(LATEX_DIR)/,, $<)
 	mv $(LATEX_DIR)/PDF.pdf $@
 
-../midnight-example.pdf: $(LATEX_DIR)/MidnightExample/PDF.tex $(latexFiles) $(PRE)
+$(OUT_DIR)/midnight-example.pdf: $(LATEX_DIR)/MidnightExample/PDF.tex $(latexFiles) $(PRE)
 	@echo "Generating $@"
 	cd $(LATEX_DIR) && $(LATEX) $(subst $(LATEX_DIR)/,, $<)
 	mv $(LATEX_DIR)/PDF.pdf $@
 
-all:
-	$(MAKE) ../cardano-ledger.pdf
-	$(MAKE) ../midnight-example.pdf
+# Agda -> HTML
+$(HTML_DIR)/Ledger.PDF.html : Ledger/PDF.lagda
+	@echo "Generating $@"
+	$(AGDA) --html --html-dir $(HTML_DIR) $<
+$(HTML_DIR)/MidnightExample.PDF.html : MidnightExample/PDF.lagda
+	@echo "Generating $@"
+	$(AGDA) --html --html-dir $(HTML_DIR) $<
+
+# Agda -> Haskell
+LEDGER_CABAL=cardano-ledger.cabal
+$(HS_DIR_LEDGER)/Foreign/HSLedger.hs: Ledger/Foreign/HSLedger.agda
+	@echo "Generating $@"
+	mkdir -p $(HS_DIR_LEDGER)
+	cp Ledger/*.hs $(HS_DIR_LEDGER)/
+	cp Ledger/$(LEDGER_CABAL) $(HS_DIR_LEDGER)/
+	$(AGDA) -c --ghc-dont-call-ghc --compile-dir $(HS_DIR_LEDGER) $<
+	find $(HS_DIR_LEDGER)/MAlonzo -name "*.hs" -print \
+	  | sed "s#^$(HS_DIR_LEDGER)/#        #;s#\.hs##;s#/#.#g" \
+	  >> $(HS_DIR_LEDGER)/$(LEDGER_CABAL)
+
+MIDNIGHT_CABAL=midnight-example.cabal
+$(HS_DIR_MIDNIGHT)/HSLedger.hs: MidnightExample/HSLedger.agda
+	mkdir -p $(HS_DIR_MIDNIGHT)
+	@echo "Generating $@"
+	cp MidnightExample/*.hs $(HS_DIR_MIDNIGHT)/
+	cp MidnightExample/$(MIDNIGHT_CABAL) $(HS_DIR_MIDNIGHT)/
+	$(AGDA) -c --ghc-dont-call-ghc --compile-dir $(HS_DIR_MIDNIGHT) $<
+	find $(HS_DIR_MIDNIGHT)/MAlonzo -name "*.hs" -print \
+	  | sed "s#^$(HS_DIR_MIDNIGHT)/#        #;s#\.hs##;s#/#.#g" \
+	  >> $(HS_DIR_MIDNIGHT)/$(MIDNIGHT_CABAL)
+
+# User commands
+docs:
+	$(MAKE) $(OUT_DIR)/cardano-ledger.pdf
+	$(MAKE) $(OUT_DIR)/midnight-example.pdf
+html:
+	$(MAKE) $(HTML_DIR)/Ledger.PDF.html
+	$(MAKE) $(HTML_DIR)/MidnightExample.PDF.html
+codeGen:
+	$(MAKE) $(HS_DIR_LEDGER)/Foreign/HSLedger.hs
+	$(MAKE) $(HS_DIR_MIDNIGHT)/HSLedger.hs
+hsBuild: $(HS_DIR_LEDGER)/Main.hs $(HS_DIR_MIDNIGHT)/Main.hs
+	cd $(HS_DIR_LEDGER)   && cabal run -- main
+	cd $(HS_DIR_MIDNIGHT) && cabal run -- main
+all: docs html codeGen hsBuild
 
 clean:
-	rm -rf $(LATEX_DIR)/Ledger/ $(LATEX_DIR)/MidnightExample \
-	       ../cardano-ledger.pdf ../midnight-example.pdf
+	rm -rf $(LATEX_DIR)/Ledger/ $(LATEX_DIR)/MidnightExample $(LATEX_DIR)/PDF.* \
+	       $(OUT_DIR)/
 
-# TODO: Agda HTML generation
-# TODO: Haskell code generation
-# TODO: use this into `default.nix` instead of repeating the same kind of commands
+# TODO: integrate into `default.nix` to remove duplication

src/MidnightExample/HSLedger.agda

@@ -14,8 +14,7 @@ import Data.Maybe
 open import Data.String using (_++_)
 
 import MidnightExample.Types as F
-
-Hash = ℕ
+open F using (Hash)
 
 instance
   Hashable-String = Hashable String Hash ∋ λ where .hash → F.hash

src/MidnightExample/Lib.hs

@@ -0,0 +1,7 @@
+module Lib
+  ( module MAlonzo.Code.MidnightExample.HSLedger
+  , module MAlonzo.Code.MidnightExample.Types
+  ) where
+
+import MAlonzo.Code.MidnightExample.HSLedger
+import MAlonzo.Code.MidnightExample.Types

src/MidnightExample/Main.hs

@@ -1,7 +1,6 @@
-module Main (module Main, module MAlonzo.Code.MidnightExample.HSLedger) where
+module Main where
 
-import MAlonzo.Code.MidnightExample.HSLedger
-import MAlonzo.Code.MidnightExample.Types
+import Lib
 
 runSteps :: (s -> sig -> Maybe s) -> s -> [sig] -> Maybe s
 runSteps f s []       = Just s

src/MidnightExample/agda-ledger-executable-spec.cabal → src/MidnightExample/midnight-example.cabal

@@ -1,5 +1,5 @@
 cabal-version:      2.4
-name:               agda-ledger-executable-spec-midnight
+name:               midnight-example
 version:            0.1.0.0
 synopsis:
 
@@ -18,22 +18,30 @@ maintainer:         [email protected]
 -- category:
 extra-source-files: CHANGELOG.md
 
+executable main
+    main-is: Main.hs
+    ghc-options: -Wno-missing-home-modules
+    build-depends:
+        base,
+        text,
+        ieee,
+        midnight-example
+
 library
     exposed-modules:
-        Main
-
-    other-extensions:
-        CPP PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
-        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
-        PatternSynonyms
-
+        Lib
     build-depends:
         base,
         text,
         ieee
-
-    ghc-options: -Wno-overlapping-patterns
-    hs-source-dirs:   .
+    hs-source-dirs: .
     default-language: Haskell2010
+    ghc-options:
+        -Wno-overlapping-patterns
+    other-extensions:
+        CPP PolyKinds EmptyDataDecls EmptyCase ExistentialQuantification
+        ScopedTypeVariables NoMonomorphismRestriction RankNTypes
+        PatternSynonyms
+
 -- This will be generated automatically when building with nix
     other-modules: