From 11459839bade6009c349cd5a06eba43f81561479 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 18 Oct 2023 01:19:54 -0600 Subject: [PATCH] PDF cleanup: remove all `\small` directives Remove all `\small` latex directives and change global Agda code font size to "small." (Some code blocks were enclosed inside `{\small ... }` which resulted in inconsistent code font size across the document.) --- src/Ledger/GovernanceActions.lagda | 10 ---------- src/Ledger/PParams.lagda | 2 -- src/Ledger/Ratify.lagda | 12 ------------ src/latex/agda.sty | 5 +++-- 4 files changed, 3 insertions(+), 26 deletions(-) diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 7f6cd7963..314a8f7f0 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -31,7 +31,6 @@ maximum : ℙ ℚ → ℚ maximum x = foldl Data.Rational._⊔_ 0ℚ (proj₁ $ finiteness x) \end{code} \begin{figure*}[h] -{\small \begin{code} GovActionID : Set GovActionID = TxId × ℕ @@ -61,7 +60,6 @@ actionWellFormed : GovAction → Bool actionWellFormed (ChangePParams x) = ppdWellFormed x actionWellFormed _ = true \end{code} -} %% end small \caption{Governance actions} \label{defs:governance} \end{figure*} @@ -157,7 +155,6 @@ Every governance action must be ratified by at least two of these three bodies u The type of action and the state of the governance system determines which bodies must ratify it. Ratified actions are then \defn{enacted} on-chain, following a set of rules (see Section~\ref{sec:enactment} and Figure~\ref{fig:enactment-types}). \begin{figure*}[h] -{\small \begin{code} NeedsHash : GovAction → Set NeedsHash NoConfidence = GovActionID @@ -171,7 +168,6 @@ NeedsHash Info = ⊤ HashProtected : Set → Set HashProtected A = A × GovActionID \end{code} -} %% end small \caption{NeedsHash and HashProtected types} \label{fig:needshash-and-hashprotected-types} \end{figure*} @@ -190,7 +186,6 @@ attached to the action we want to ratify. See Section~\ref{sec:ratification} for more on the ratification process. \begin{figure*}[h] -{\small \begin{code} data Vote : Set where yes no abstain : Vote @@ -209,7 +204,6 @@ record GovProposal : Set where deposit : Coin anchor : Anchor \end{code} -} %% end small \caption{Governance action proposals and votes} \label{defs:governance-votes} \end{figure*} @@ -257,7 +251,6 @@ A record of type \EnactState represents the state for enacting a governance acti The latter contains fields for the constitutional committee, constitution, protocol version, protocol parameters, withdrawals from treasury, and treasury balance. \begin{figure*}[h] -{\small \begin{code} record EnactEnv : Set where constructor ⟦_,_,_⟧ᵉ @@ -276,7 +269,6 @@ ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credenti ccCreds (just x , _) = dom (x .proj₁) ccCreds (nothing , _) = ∅ \end{code} -} %% end small \caption{Enactment types} \label{fig:enactment-types} \end{figure*} @@ -310,7 +302,6 @@ The relation \ENACTsyntax is the transition relation for enacting a governance a It represents how the \agdaboundEnactState changes when a specific governance action is enacted (see Figure~\ref{fig:enact-transition-system}). \begin{figure*}[h] -{\small \begin{code} data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Set where @@ -345,7 +336,6 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta Enact-Info : ⟦ gid , t , e ⟧ᵉ ⊢ s ⇀⦇ Info ,ENACT⦈ s \end{code} -} %% end small \caption{ENACT transition system} \label{fig:enact-transition-system} \end{figure*} diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index 13ff6f74f..baef784b8 100644 --- a/src/Ledger/PParams.lagda +++ b/src/Ledger/PParams.lagda @@ -23,7 +23,6 @@ module Ledger.PParams where \end{code} \begin{figure*}[h!] -{\small \begin{AgdaAlign} \begin{code} ProtVer : Set @@ -99,7 +98,6 @@ paramsWellFormed pp = 0 ∉ fromList where open PParams pp \end{code} \end{AgdaAlign} -} %% End: small \caption{Protocol parameter declarations} \label{fig:protocol-parameter-declarations} \end{figure*} diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 34c0ef4a5..c7e5e28f2 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -99,7 +99,6 @@ instance _ = +-0-monoid \end{code} \begin{figure*}[h!] -{\small \begin{code} record StakeDistrs : Set where field stakeDistr : VDeleg ⇀ Coin @@ -144,7 +143,6 @@ isDRepProp = to-sp (λ x → isDRep x ≟ true) isSPOProp : specProperty λ x → isSPO x ≡ true isSPOProp = to-sp (λ x → isSPO x ≟ true) \end{code} -} %% end small \caption{Types and functions for the RATIFY transition system} \label{fig:types-and-functions-for-the-ratify-transition-system} \end{figure*} @@ -232,7 +230,6 @@ restrictedDists coins rank dists = dists restrict dist = topNDRepDist rank dist ∪ᵐˡ mostStakeDRepDist dist coins \end{code} \begin{figure*}[h!] -{\small \begin{code} actualVotes : RatifyEnv → CCData → (GovRole × Credential) ⇀ Vote → GovAction → PParams → VDeleg ⇀ Vote @@ -287,7 +284,6 @@ actualVotes Γ cc votes ga pparams (TriggerHF _) → true _ → false \end{code} -} %% end small \caption{%Ratify i: Types and proofs for the ratification of governance actions} \label{fig:defs:ratify-i} @@ -323,7 +319,6 @@ The code in Figure~\ref{fig:defs:ratify-i} defines some of the types required fo it accomplishes this by aggregating the results of \actualCCVotes, \actualPDRepVotes, and \actualDRepVotes. \end{itemize} \begin{figure*}[h!] -{\small \begin{code} votedHashes : Vote → (VDeleg ⇀ Vote) → GovRole → ℙ VDeleg votedHashes v votes r = votes ⁻¹ v @@ -335,14 +330,12 @@ votedAbstainHashes participatingHashes : (VDeleg ⇀ Vote) → GovRole → ℙ V votedAbstainHashes = votedHashes Vote.abstain participatingHashes votes r = votedYesHashes votes r ∪ votedHashes Vote.no votes r \end{code} -} %% end small \caption{Calculation of the votes as they will be counted} \label{fig:defs:ratify-ii} \end{figure*} The code in Figure~\ref{fig:defs:ratify-ii} defines \votedHashes, which returns the set of delegates who voted a certain way on the given governance role. \begin{figure*}[h!] -{\small \begin{code}[hide] abstract \end{code} @@ -381,7 +374,6 @@ abstract expired : Epoch → GovActionState → Set expired current record { expiresIn = expiresIn } = expiresIn < current \end{code} -} %% end small \caption{%%Ratify iii: Calculation of stake distributions} \label{fig:defs:ratify-iii} @@ -397,7 +389,6 @@ The code in Figure~\ref{fig:defs:ratify-iii} defines yet more types required for \item \expired checks whether a governance action is expired in a given epoch. \end{itemize} \begin{figure*}[h!] -{\small \begin{code}[hide] open EnactState \end{code} @@ -455,7 +446,6 @@ abstract expired? : ∀ e st → Dec (expired e st) expired? e st = ¿ expired e st ¿ \end{code} -} %% end small \caption{%Ratify iv: Determination of the status of ratification of the governance action} \label{fig:defs:ratify-iv} @@ -479,7 +469,6 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov \end{code} \begin{figure*}[h!] -{\small \begin{code} RATIFY-Accept : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in accepted Γ es st @@ -507,7 +496,6 @@ _⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → List (GovActionID × Go → RatifyState → Set _⊢_⇀⦇_,RATIFY⦈_ = SS⇒BS _⊢_⇀⦇_,RATIFY'⦈_ \end{code} -} %% end small \caption{The RATIFY transition system} \label{fig:ratify-transition-system} \end{figure*} diff --git a/src/latex/agda.sty b/src/latex/agda.sty index 58c28ec8a..59e0d2885 100644 --- a/src/latex/agda.sty +++ b/src/latex/agda.sty @@ -358,8 +358,9 @@ % ---------------------------------------------------------------------- % The code environment. -\newcommand{\AgdaCodeStyle}{} -% \newcommand{\AgdaCodeStyle}{\tiny} +%\newcommand{\AgdaCodeStyle}{} +\newcommand{\AgdaCodeStyle}{\small} +%\newcommand{\AgdaCodeStyle}{\tiny} \ifdefined\mathindent {}