Vendor fonts from formal-ledger-specification

These are needed as the Agda source contains quite a lot of unicode which the font needs to be able to display.
cardano-scaling · Aug 20, 2024 · 1181d7b · 1181d7b
1 parent cd966a0
commit 1181d7b
Show file tree

Hide file tree

Showing 21 changed files with 79 additions and 48 deletions.
diff --git a/Shakefile.hs b/Shakefile.hs
@@ -13,17 +13,17 @@ main = shakeArgs shakeOptions{shakeFiles="_build"} $ do
       removeFilesAfter "_build" ["//*"]
 
     "_build/hydra-spec" <.> "pdf" %> \out -> do
-      assets <- getDirectoryFiles "src" ["//*.sty", "Hydra/Protocol/Figures/*.pdf", "//*.bib"]
+      assets <- getDirectoryFiles "src" ["//*.sty", "Hydra/Protocol/Figures/*.pdf", "//*.bib", "//*.ttf"]
       need ["_build/latex" </> c | c <- assets]
 
       srcs <- getDirectoryFiles "src" ["//*.lagda", "//*.tex"]
       need ["_build/latex" </> c -<.> "tex" | c <- srcs]
 
-      cmd_ (Cwd "_build/latex") "latexmk -xelatex Hydra/Protocol/Main.tex"
+      cmd_ (Cwd "_build/latex") "latexmk -xelatex -shell-escape -halt-on-error Hydra/Protocol/Main.tex"
       cmd_ "cp _build/latex/Main.pdf _build/hydra-spec.pdf"
 
     -- Copy assets
-    forM ["sty", "pdf", "bib"] $ \ext ->
+    forM ["sty", "pdf", "bib", "ttf"] $ \ext ->
       ("_build/latex//*." <> ext)  %> \out -> do
         let src = "src" </> dropDirectory1 (dropDirectory1 out)
         copyFile' src out

diff --git a/src/Hydra/Protocol/Main.lagda b/src/Hydra/Protocol/Main.lagda
@@ -1,49 +1,7 @@
 \documentclass[11pt]{article}
 
-\usepackage{amsfonts,amsmath,amssymb,amsthm}
-\usepackage[normalem]{ulem} % temporary for strikeout math
-\usepackage{enumerate}
-\usepackage[shortlabels,inline]{enumitem}
-\usepackage{wrapfig}
-
-\usepackage[lined,noend]{algorithm2e}
-\usepackage{tabularx}
-\usepackage{colortbl}
-\usepackage{adjustbox}
-\DontPrintSemicolon
-
-\PassOptionsToPackage{hyphens}{url}
-\usepackage{fullpage}
-\usepackage{hyperref}
-\usepackage{xcolor}
-\usepackage{xifthen}
-% Keep figures in same section
-\usepackage[section]{placeins}
-\usepackage{pifont}
-\usepackage{multirow}
-\usepackage{tikz}
-\usetikzlibrary{automata, arrows}
-\usepackage{pgfplots}
-\usepackage[framemethod=tikz]{mdframed} % and thus tikz
-\usepackage[font=small]{caption}
-\usepackage[many]{tcolorbox}    	% for COLORED BOXES
-
-\usepackage{authblk}
-
-% footnotes in table and tabular
-\usepackage{footnote}
-\makesavenoteenv{tabular}
-\makesavenoteenv{table}
-\makesavenoteenv{figure}
-
-\usepackage{stmaryrd} % fancy double square brackets
-\usepackage{todonotes}
-
-\setcounter{tocdepth}{2} % Override LLNCS
-
-\usepackage{agda}
-
-\include{Hydra/Protocol/Macros}
+\include{preamble}
+\include{macros}
 
 \begin{document}
 

diff --git a/src/Hydra/Protocol/Preliminaries.tex b/src/Hydra/Protocol/Preliminaries.tex
@@ -31,7 +31,7 @@ \subsection{Notation}
 \begin{itemize}
 	\item $\tyBool = \{\false, \true\}$ are boolean values
 	\item $\tyNatural$ are natural numbers $\{0, 1, 2, \ldots\}$
-	\item $\tyInteger$ are integer numbers $\{\ldots, −2, −1, 0, 1, 2, \ldots\}$
+	\item $\tyInteger$ are integer numbers $\{\ldots, -2, -1, 0, 1, 2, \ldots\}$
 	\item $\tyBytes = \bigcup_{n=0}^{\inf}{\{0,1\}}^{8n}$ denotes a arbitrary
 	      string of bytes
 	\item $\concat : \tyBytes^* \to \tyBytes$ is concatenating bytes, we also use operator $\bigoplus$ for this

diff --git a/src/fonts/StrippedJuliaMono-Black.ttf b/src/fonts/StrippedJuliaMono-Black.ttf
diff --git a/src/fonts/StrippedJuliaMono-BlackItalic.ttf b/src/fonts/StrippedJuliaMono-BlackItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-Bold.ttf b/src/fonts/StrippedJuliaMono-Bold.ttf
diff --git a/src/fonts/StrippedJuliaMono-BoldItalic.ttf b/src/fonts/StrippedJuliaMono-BoldItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-BoldLatin.ttf b/src/fonts/StrippedJuliaMono-BoldLatin.ttf
diff --git a/src/fonts/StrippedJuliaMono-ExtraBold.ttf b/src/fonts/StrippedJuliaMono-ExtraBold.ttf
diff --git a/src/fonts/StrippedJuliaMono-ExtraBoldItalic.ttf b/src/fonts/StrippedJuliaMono-ExtraBoldItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-Light.ttf b/src/fonts/StrippedJuliaMono-Light.ttf
diff --git a/src/fonts/StrippedJuliaMono-LightItalic.ttf b/src/fonts/StrippedJuliaMono-LightItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-Medium.ttf b/src/fonts/StrippedJuliaMono-Medium.ttf
diff --git a/src/fonts/StrippedJuliaMono-MediumItalic.ttf b/src/fonts/StrippedJuliaMono-MediumItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-Regular.ttf b/src/fonts/StrippedJuliaMono-Regular.ttf
diff --git a/src/fonts/StrippedJuliaMono-RegularItalic.ttf b/src/fonts/StrippedJuliaMono-RegularItalic.ttf
diff --git a/src/fonts/StrippedJuliaMono-RegularLatin.ttf b/src/fonts/StrippedJuliaMono-RegularLatin.ttf
diff --git a/src/fonts/StrippedJuliaMono-SemiBold.ttf b/src/fonts/StrippedJuliaMono-SemiBold.ttf
diff --git a/src/fonts/StrippedJuliaMono-SemiBoldItalic.ttf b/src/fonts/StrippedJuliaMono-SemiBoldItalic.ttf
diff --git a/src/Hydra/Protocol/Macros.tex → src/macros.tex b/src/Hydra/Protocol/Macros.tex → src/macros.tex
diff --git a/src/preamble.tex b/src/preamble.tex
@@ -0,0 +1,73 @@
+% Common packages and settings
+% Many things here are from the original hydra paper or from the formal-ledger-specifications
+
+\usepackage{amsfonts,amsmath,amssymb,amsthm}
+\usepackage[normalem]{ulem} % temporary for strikeout math
+\usepackage{enumerate}
+\usepackage[shortlabels,inline]{enumitem}
+\usepackage{wrapfig}
+
+\usepackage[lined,noend]{algorithm2e}
+\usepackage{tabularx}
+\usepackage{colortbl}
+\usepackage{adjustbox}
+\DontPrintSemicolon
+
+\PassOptionsToPackage{hyphens}{url}
+\usepackage{fullpage}
+\usepackage{hyperref}
+\usepackage{xcolor}
+\usepackage{xifthen}
+% Keep figures in same section
+\usepackage[section]{placeins}
+\usepackage{pifont}
+\usepackage{multirow}
+\usepackage{tikz}
+\usetikzlibrary{automata, arrows}
+\usepackage{pgfplots}
+\usepackage[framemethod=tikz]{mdframed} % and thus tikz
+\usepackage[font=small]{caption}
+\usepackage[many]{tcolorbox}    	% for COLORED BOXES
+
+\usepackage{authblk}
+
+% footnotes in table and tabular
+\usepackage{footnote}
+\makesavenoteenv{tabular}
+\makesavenoteenv{table}
+\makesavenoteenv{figure}
+
+\usepackage{stmaryrd} % fancy double square brackets
+\usepackage{todonotes}
+
+\setcounter{tocdepth}{2} % Override LLNCS
+
+% Highlighted agda code
+\usepackage[links]{agda}
+
+% Use a font that works well with agda
+% NOTE: Vendored from formal-ledger-specifications
+\usepackage{fontspec}
+\newcommand\agdaFont{StrippedJuliaMono}
+\newcommand\agdaFontOptions{
+Path=fonts/,
+Extension=.ttf,
+UprightFont=*-Regular,
+BoldFont=*-Bold,
+ItalicFont=*-RegularItalic,
+BoldItalicFont=*-BoldItalic,
+Scale=0.80
+}
+\newfontfamily{\AgdaSerifFont}{\agdaFont}[\agdaFontOptions]
+\newfontfamily{\AgdaSansSerifFont}{\agdaFont}[\agdaFontOptions]
+\newfontfamily{\AgdaTypewriterFont}{\agdaFont}[\agdaFontOptions]
+\renewcommand{\AgdaFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
+\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
+\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
+\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
+\renewcommand{\AgdaBoundFontStyle}[1]{{\emph{\AgdaTypewriterFont{}#1}}}
+
+% Also use unicode compatible math fonts
+\usepackage{unicode-math}
+\setsansfont{XITSMath-Regular.otf}
+\setmathfont{XITSMath-Regular.otf}