effect Carlos's change requests plus miscellaneous improvements

+ fix mkdocs hang issue
+ move EssentialAgda
+ switch to unicode character for em dash
+ fix broken links
+ revert removal of latex packages in flake (needed for diagram generation)
+ remove repeated console log
+ rename "Agda Essentials" -> "Essential Agda" to agree with module name
+ make reference-able NEWEPOCH section and add link to it
+ improve introduction and remove references to pdf generation

Author: williamdemeo

build-tools/scripts/md/build.py

@@ -67,7 +67,6 @@ def main(run_agda_html_flag: bool = False, test_mode_flag: bool = False) -> None
     if static_tex_result.is_err:
         logging.error(f"❌ Static LaTeX conversion failed: {static_tex_result.unwrap_err()}")
         sys.exit(1)
-    logging.info(f"✅ Converted {len(static_tex_result.unwrap())} static .tex files to Markdown")
 
     # 4. Process Agda source files (.agda -> .lagda.md)
     agda_result = process_agda_source_files(config)

build-tools/static/md/mkdocs/includes/links.md

@@ -1,5 +1,4 @@
 [Agda documentation]: https://agda.readthedocs.io/en/
-[Agda Essentials]: Ledger.EssentialAgda.md
 [Agda record types]: https://agda.readthedocs.io/en/stable/language/record-types.html
 [Agda Wiki]: https://wiki.portal.chalmers.se/agda/pmwiki.php
 [Amount of Rewards to be Paid Out]: Ledger.Conway.Specification.Rewards.md#sec:amount-of-rewards-to-be-paid-out
@@ -22,9 +21,12 @@
 [DELEG]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system
 [ENACT]: Ledger.Conway.Specification.Enact.md#sec:the-enact-transition-system
 [EPOCH]: Ledger.Conway.Specification.Epoch.md#sec:the-epoch-transition-system
+[Epoch]: Ledger.Conway.Specification.Epoch.md
+[Epoch Boundary]: Ledger.Conway.Specification.Epoch.md#sec:epoch-boundary
 [Epoch.Properties.ConstRwds]: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md
 [Epoch.Properties.GovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md
 [Epoch.Properties.NoPropSameDReps]: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md
+[Essential Agda]: EssentialAgda.md
 [Fees]: Ledger.Conway.Specification.Fees.md
 [formal ledger specification]: https://github.com/IntersectMBO/formal-ledger-specifications
 [Functions used in UTxO rules]: Ledger.Conway.Specification.Utxo.md#functions-used-in-utxo-rules
@@ -41,15 +43,18 @@
 [LEDGERS]: Ledger.Conway.Specification.Ledger.md#ledgers-transition-system
 [lem:EpochGovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md#lem:EpochGovDepsMatch
 [lem:LedgerGovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md#lem:LedgerGovDepsMatch
+[NEWEPOCH]: Ledger.Conway.Specification.Epoch.md#sec:the-newepoch-transition-system
 [Notation]: Notation.md
 [Ouroboros Chronos blog post]: https://iohk.io/en/blog/posts/2021/10/27/ouroboros-chronos-provides-the-first-high-resilience-cryptographic-time-source-based-on-blockchain/
 [POOL]: Ledger.Conway.Specification.Certs.md#auxiliary-pool-transition-system
-[Protocol Parameter Decfinitions]: Ledger.Conway.Specification.PParams.md#sec:protocol-parameter-definitions
+[Protocol Parameter Definitions]: Ledger.Conway.Specification.PParams.md#sec:protocol-parameter-definitions
 [Ratification Requirements]: Ledger.Conway.Specification.Ratify.md#sec:ratification-requirements
 [RATIFY]: Ledger.Conway.Specification.Ratify.md#the-ratify-transition-system
 [(Re)introduction to Cardano]: https://developers.cardano.org/docs/operate-a-stake-pool/introduction-to-cardano/
 [repourl]: https://github.com/IntersectMBO/formal-ledger-specifications
+[Rewards Calculation Timeline]: Ledger.Conway.Specification.Rewards.md#sec:rewards-calculation-timeline
 [Rewards Motivation]: Ledger.Conway.Specification.Rewards.md#sec:rewards-motivation
+[Script Validation]: Ledger.Conway.Specification.Script.Validation.md#sec:script-validation
 [scriptsCost]: Ledger.Conway.Specification.Fees.md#scriptsCost
 [Shelley Ledger Spec (pdf)]: https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf
 [SNAP]: Ledger.Conway.Specification.Rewards.md#sec:snap-transition-system
@@ -63,6 +68,6 @@
 [Utxo.Properties.PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md
 [UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:the-utxos-transition-rule
 [UTXOW]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
+[Utxow module]: Ledger.Conway.Specification.Utxow.md
 [Validity and wellformedness predicates]: Ledger.Conway.Specification.Gov.md#validity-and-wellformedness-predicates
-[Voting Functions]: Ledger.Conway.Specification.Ratify.md#sec:voting-functions
 

build-tools/static/md/mkdocs/mkdocs.yml

@@ -86,6 +86,7 @@ extra_javascript:
 markdown_extensions:
   - admonition                # call-out boxes like !!! note
   - pymdownx.details
+  - pymdownx.smartsymbols
   - toc:                      # table of contents generation
       permalink: true         # anchor links to headers
   - pymdownx.superfences:     # syntax highlighting in code blocks

build-tools/static/md/nav.yml

@@ -215,7 +215,7 @@
       - Deriving: Foreign.HaskellTypes.Deriving.md
   - Appendix/:
     - Definitions: Definitions.md
-    - EssentialAgda: Ledger.EssentialAgda.md
+    - EssentialAgda: EssentialAgda.md
     - Agda Prelude: Prelude.md
     - Type Classes:
       - Interface:

flake.nix

@@ -122,6 +122,10 @@
                   inherit (texlive)
                     scheme-small
                     dejavu
+                    collection-latexextra
+                    collection-latexrecommended
+                    collection-mathscience
+                    bclogo
                     luatex
                     luatex85
                     dvisvgm

src/Ledger/EssentialAgda.lagda.md src/EssentialAgda.lagda.mdsrc/Ledger/EssentialAgda.lagda.md renamed to src/EssentialAgda.lagda.md

@@ -3,7 +3,7 @@ source_branch: master
 source_path: src/EssentialAgda.lagda.md
 ---
 
-# Agda Essentials {#sec:agda-essentials}
+# Essential Agda {#sec:essential-agda}
 
 Here we describe some of the essential concepts and syntax of the Agda
 programming language and proof assistant. The goal is to provide some
@@ -17,7 +17,7 @@ details, the reader is encouraged to consult the official
 ```agda
 {-# OPTIONS --safe #-}
 
-module Ledger.EssentialAgda where
+module EssentialAgda where
 
 open import Prelude using (Type)
 open import Data.Nat

src/Interface/STS.lagda.md

@@ -31,7 +31,7 @@ private
 ## A Note on Recent Changes
 
 We refactored the `STS`{.AgdaModule} module to reflect what the code actually
-does---it processes a list of signals, transforming state.
+does--it processes a list of signals, transforming state.
 
 +  **Clearer names**
 
@@ -48,7 +48,7 @@ does---it processes a list of signals, transforming state.
 +  `RunTraceAndThen Step Last Γ s sigs s'` means: starting in `s`, running `sigs`
    (left-to-right) under environment `Γ`, then perform `Last`, to yield `s'`.
 
-A variation that is sometimes useful involves indexed steps---that is, it allows the
+A variation that is sometimes useful involves indexed steps--that is, it allows the
 step relation to depend on the position in the trace via an index `n : ℕ`.
 
 ## State Transition Sytem Types

src/Ledger.agda

@@ -4,4 +4,4 @@ import Ledger.Introduction
 import Ledger.PreConway
 import Ledger.Conway
 
-import Ledger.EssentialAgda
+import EssentialAgda

src/Ledger/Conway/Specification/Certs.lagda.md

@@ -418,7 +418,7 @@ Sections [Auxiliary `DELEG`{.AgdaDatatype} Transition System](#auxiliary-deleg-t
 [Auxiliary `GOVCERT`{.AgdaDatatype} transition system](#auxiliary-govcert-transition-system).
 
 `GOVCERT`{.AgdaDatatype} deals with the new certificates relating to
-`DRep`{.AgdaInductiveConstructor}s and the constitutional committee.
+`DReps`{.AgdaInductiveConstructor} and the constitutional committee.
 
 +  `GOVCERT-regdrep`{.AgdaInductiveConstructor} registers (or
    re-registers) a `DRep`{.AgdaInductiveConstructor}.  In case of registration,
@@ -541,7 +541,7 @@ important housekeeping tasks:
 +  check the correctness of withdrawals and ensure that withdrawals only
    happen from credentials that have delegated their voting power;
 
-+  set the activity timer of all `DRep`{.AgdaInductiveConstructor}s that voted
++  set the activity timer of all `DReps`{.AgdaInductiveConstructor} that voted
    to `drepActivity`{.AgdaField} epochs in the future;
 
 +  set the rewards of the credentials that withdrew funds to zero.

src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md

@@ -61,8 +61,8 @@ module Certs-PoV  ( indexedSumᵛ'-∪' :  {A : Type} ⦃ _ : DecEq A ⦄ (m m'
 
 *Informally*.
 
-Let `l`{.AgdaBound} be a list of `DCert`{.AgdaDatatype}s, and let `s₁`{.AgdaBound},
-`sₙ`{.AgdaBound} be `CertState`{.AgdaRecord}s such that
+Let `l`{.AgdaBound} be a list of `DCerts`{.AgdaDatatype}, and let `s₁`{.AgdaBound},
+`sₙ`{.AgdaBound} be `CertStates`{.AgdaRecord} such that
 `s₁`{.AgdaBound} `⇀⦇`{.AgdaDatatype} `l`{.AgdaBound} `,CERTS⦈`{.AgdaDatatype} `sₙ`{.AgdaBound}.
 Then, the value of `s₁`{.AgdaBound} is equal to the value of `sₙ`{.AgdaBound} plus
 the value of the withdrawals in `Γ`{.AgdaBound}.