adopt new build, add sts png, add global links

Author: William DeMeo

mkdocs/src/docs/Notation.md

@@ -26,7 +26,7 @@ The *sum* (or disjoint union, coproduct, etc.) of `A`{.agdabound} and
 `B`{.agdabound} is denoted by
 `A`{.agdabound} `⊎`{.agdadatatype} `B`{.agdabound}, and their product
 is denoted by `A`{.agdabound} `×`{.agdafunction} `B`{.agdabound}. The 
-projection functions from products are denoted \fst{} and \snd{}, 
+projection functions from products are denoted
 `proj₁`{.agdafield} and `proj₂`{.agdafield} and the injections are denoted
 `inj₁`{.agdainductiveconstructor} and
 `inj₂`{.agdainductiveconstructor}, respectively. The
@@ -60,7 +60,6 @@ write
 `.`{.agdasymbol}
 `proj₁`{.agdafield}
 instead of
-
 `proj₁`{.agdafield}
 `x`{.agdabound}
 
@@ -201,6 +200,6 @@ and can safely be ignored. However there are the two exceptions:
 
 - `ᶜ`{.agdafunction}in the context of set restrictions, where it indicates the complement
 
-Also, non-letter superscripts do carry meaning.[^1]
+Also, non-letter superscripts do carry meaning.
 
-[^1]: At some point in the future we hope to be able to remove all those non-essential superscripts. Since we prefer doing this by changing the Agda source code instead of via hiding them in this document, this is a non-trivial problem that will take some time to address.
+(At some point in the future we hope to be able to remove all those non-essential superscripts. Since we prefer doing this by changing the Agda source code instead of via hiding them in this document, this is a non-trivial problem that will take some time to address.)

mkdocs/src/docs/img/STS-diagram.png

@@ -0,0 +1,28 @@
+[Agda documentation]: https://agda.readthedocs.io/en/
+[Agda Essentials]: EssentialAgda.md
+[Agda Wiki]: https://wiki.portal.chalmers.se/agda/pmwiki.php
+[Auxiliary DELEG transition system]: Ledger.Conway.Certs.md#auxiliary-deleg-transition-system
+[Auxiliary GOVCERT transition system]: Ledger.Conway.Certs.md#auxiliary-govcert-transition-system
+[Auxiliary POOL transition system]: Ledger.Conway.Certs.md#auxiliary-pool-transition-system
+[CERT]: Ledger.Conway.Certs.md#certs-rules
+[CERTS]: Ledger.Conway.Certs.md#certs-rules
+[CERTS rules]: Ledger.Conway.Certs.md#certs-rules
+[CHAIN]: Ledger.Conway.Chain.md#chain-transition-system
+[DELEG]: Ledger.Conway.Certs.md#auxiliary-deleg-transition-system
+[ENACT]: Ledger.Conway.Enact.md#enact-transition-system
+[EPOCH]: Ledger.Conway.Epoch.md#epoch-transition-system
+[GOV]: Ledger.Conway.Gov.md#rules-for-the-gov-transition-system
+[GOVCERT]: Ledger.Conway.Certs.md#auxiliary-govcert-transition-system
+[issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues
+[LEDGER]: Ledger.Conway.Ledger.md#ledger-transition-system
+[LEDGERS]: Ledger.Conway.Ledger.md#ledgers-transition-system
+[NEWEPOCH]: Ledger.Conway.Epoch.md#newepoch-transition-system
+[Notation]: Notation.md
+[POOL]: Ledger.Conway.Certs.md#auxiliary-pool-transition-system
+[RATIFY]: Ledger.Conway.Ratify.md#the-ratify-transition-system
+[repourl]: https://github.com/IntersectMBO/formal-ledger-specifications
+[SNAP]: Ledger.Conway.Rewards.md#snap-transition-system
+[UTXO]: Ledger.Conway.Utxo.md#utxo-inference-rules
+[UTXOS]: Ledger.Conway.Utxo.md#utxos-rule
+[UTXOW]: Ledger.Conway.Utxow.md#utxow-inference-rules
+[Shelley Ledger Spec (pdf)]: https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf

mkdocs/src/includes/links.md

@@ -17,18 +17,14 @@ theme:
     - toc.integrate # Integrate table of contents into left sidebar
     - content.tooltips
     - navigation.footer
-  # palette: # Optional: color scheme
-  #   primary: indigo
-  #   accent: indigo
-
   palette:
     # Dark Mode
     - scheme: slate
       toggle:
         icon: material/weather-sunny
         name: Dark mode
-      primary: black
-      accent: red
+      primary: black # indigo
+      accent: red    # indigo
 
     # Light Mode
     - scheme: default
@@ -38,35 +34,42 @@ theme:
       primary: blue
       accent: deep orange
 
-  # Font configuration (optional)
+  # Font configuration
   font:
     text: Cambria
     code: Source Code Pro
-  #   text: Roboto
-  #   code: Roboto Mono # Or perhaps StrippedJuliaMono if available via CSS?
 
+extra_css:
+  - css/custom.css
+  - css/Agda.css
 
-# Navigation structure
-nav:
-  - Home: index.md
+extra_javascript:
+  - js/custom.js
+  - https://unpkg.com/mathjax@3/es5/tex-mml-chtml.js
 
-# Markdown extensions
 markdown_extensions:
-  - admonition                # call-out boxes like !!! note
+  - pymdownx.arithmatex:
+      generic: true
+  - admonition
   - pymdownx.details
-  - toc:                      # table of contents generation
-      permalink: true         # anchor links to headers
-  - pymdownx.superfences:     # syntax highlighting in code blocks
+  - toc:
+      permalink: "#"
+  - pymdownx.superfences:
       custom_fences:
-        - name: mermaid       # mermaid diagrams
+        - name: mermaid
           class: mermaid
-  - attr_list                 # inline attributes like `code`{.class}
-  - pymdownx.tabbed
+  - attr_list
   - pymdownx.emoji
+  - pymdownx.snippets:
+      check_paths: true  # for debugging
+      auto_append:
+        - includes/links.md
 
-extra_css:
-  - css/custom.css
-  - css/Agda.css
+watch:
+  - includes
 
-extra_javascript:
-  - js/custom.js
+use_directory_urls: false
+
+# Navigation structure
+nav:
+  - Home: index.md