Migrate all remaining lagda files

CONTRIBUTING.md

@@ -102,32 +102,33 @@ The main directories and files involved in the build process are as follows. (A
 detailed version of this annotated tree can be found at the bottom of this page.)
 
 ```
-├── flake.nix                  # Nix flake
-└── build-tools/
+├── flake.nix                  # The main Nix flake file.
+│
+└── build-tools
     ├── agda/
-    │   ├── flake.nix          # Nix flake
     │   ├── data/
-    │   │   ├── Agda.css       # for styling Agda HTML output
-    │   │   └── AgdaKaTeX.js   # for integrating Agda's HTML with KaTeX
-    │   ├── fls-agda.cabal     # for building fls-agda Haskell package
+    │   │   ├── Agda.css       # For styling Agda HTML output.
+    │   │   └── AgdaKaTeX.js   # For integrating Agda's HTML with KaTeX.
+    │   ├── flake.nix          # Auxiliary Nix flake file.
+    │   ├── fls-agda.cabal     # For building fls-agda Haskell package.
     │   ├── nix/
-    │   │   └── fls-agda.nix   # Nix derivation for fls-agda package
+    │   │   └── fls-agda.nix   # Nix derivation for fls-agda package.
     │   └── src/
-    │       └── Main.hs        # Main entry point for fls-agda executable
+    │       └── Main.hs        # Main entry point for fls-agda executable.
     │
-    ├── nix                    # Nix derivations for exported packages
+    ├── nix/                   # Nix derivations for exported packages.
     │   ├── formal-ledger.nix
     │   ├── hs-src.nix
     │   ├── html.nix
     │   └── mkdocs.nix
     │
     └── shake/
-        ├── flake.nix          # Nix flake
-        ├── fls-shake.cabal    # for building fls-shake Haskell package
+        ├── flake.nix          # Auxiliary Nix flake file.
+        ├── fls-shake.cabal    # For building fls-shake Haskell package.
         ├── nix/
-        │   └── fls-shake.nix  # Nix derivation for fls-shake package
+        │   └── fls-shake.nix  # Nix derivation for fls-shake package.
         └── src/
-            └── Main.hs        # Main entry point for fls-shake build system
+            └── Main.hs        # Main entry point for fls-shake build system.
 ```
 
 ---
@@ -446,7 +447,7 @@ the `update-alternatives` approach.)
 
     ```bash
     nix develop
-    emacs src/Ledger.agda
+    emacs src/Ledger.lagda.md
     ```
 
 3.  Use standard `agda-mode` commands (e.g., `C-c C-l` to load a file).

build-tools/nix/formal-ledger.nix

@@ -28,7 +28,7 @@ mkDerivation {
     iog-prelude
   ];
   buildPhase = ''
-    agda --profile=modules src/Ledger.agda | tee typecheck.log
+    agda --profile=modules src/Ledger.lagda.md | tee typecheck.log
   '';
   doCheck = true;
   checkPhase = ''

build-tools/nix/html.nix

@@ -8,7 +8,6 @@ mkDerivation {
   LANG = "en_US.UTF-8";
   LC_ALL = "en_US.UTF-8";
   LOCALE_ARCHIVE = lib.optionalString stdenv.isLinux "${glibcLocales}/lib/locale/locale-archive";
-
   pname = "html";
   src = lib.fileset.toSource {
     root = ../../.;

build-tools/nix/mkdocs.nix

@@ -1,14 +1,16 @@
 {
   lib,
   mkDerivation,
+  fls-agdaWithPackages,
   dejavu_fonts,
   ghostscript,
   pandoc,
   python3,
   texlive,
 }:
 mkDerivation {
-  pname = "mkdocs";
+  name = "mkdocs";
+  version = "0.1";
   src = lib.fileset.toSource {
     root = ../../.;
     fileset = lib.fileset.unions [
@@ -24,6 +26,9 @@ mkDerivation {
   };
   meta = { };
   buildInputs = [
+    dejavu_fonts
+    fls-agdaWithPackages
+    ghostscript
     pandoc
     (python3.withPackages (
       ps: with ps; [
@@ -51,8 +56,6 @@ mkDerivation {
         pgfplots
         ;
     })
-    dejavu_fonts
-    ghostscript
   ];
   buildPhase = ''
     runHook preBuild

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/docs/css/custom.css

@@ -189,3 +189,14 @@ body.reveal-agda-source pre.Agda.hidden-source {
 }
 
 .svg-card img { display:block; max-width:100%; height:auto; }
+
+
+/* ======================================================================= */
+/* Make main content region wider */
+.md-main__inner {
+  max-width: 78rem;  /* default ~72rem */
+}
+/* Tighten sidebars slightly. */
+.md-sidebar--secondary {
+  width: 14rem; /* default ~15rem */
+}

build-tools/static/md/mkdocs/hooks/agda_source_link.py

@@ -49,7 +49,7 @@
 ----------------------------
 Add something like this to any generated Markdown for which the true source is known:
 ---
-source_path: src/Ledger/Prelude.agda
+source_path: src/Ledger/Prelude.lagda.md
 source_branch: master
 ---
 

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

@@ -10,67 +10,66 @@
 [CERT]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
 [CERTS]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
 [CERTS rules]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system
-[CHAIN]: Ledger.Conway.Specification.Chain.md#chain-transition-system
+[Certs.Properties.PoV]: Ledger.Conway.Specification.Certs.Properties.PoV.md
+[Certs.Properties.PoVLemmas]: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md
+[Certs.Properties.VoteDelegsVDeleg]: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md
+[CHAIN]: Ledger.Conway.Specification.Chain.md#sec:the-chain-transition-system
 [CIPs]: https://github.com/cardano-foundation/CIPs
+[Chain.Properties.CredDepsEqualDomRwds]: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md
+[Chain.Properties.EpochStep]: Ledger.Conway.Specification.Chain.Properties.EpochStep.md
+[Chain.Properties.PParamsWellFormed]: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md
+[Chain.Properties.GovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md
 [DELEG]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system
-[ENACT]: Ledger.Conway.Specification.Enact.md#enact-transition-system
-[EPOCH]: Ledger.Conway.Specification.Epoch.md#epoch-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
-[Functions of the GOV Transition System]: Ledger.Conway.Specification.Gov.md#governance-functions
-[Functions related to voting]: Ledger.Conway.Specification.Ratify.md#functions-related-to-voting
+[Governance Functions]: Ledger.Conway.Specification.Gov.md#governance-functions
+[Governance Actions]: Ledger.Conway.Specification.Gov.Actions.md#sec:governance-actions
 [GOV]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
+[Gov.Properties.ChangePPGroup]: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md
 [GOVCERT]: Ledger.Conway.Specification.Certs.md#auxiliary-govcert-transition-system
 [Governance Functions]: Ledger.Conway.Specification.Gov.md#governance-functions
 [issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues
 [LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system
-[Ledger.Conway.Specification.Enact]: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Conway/Specification/Enact.lagda.md
-[Ledger.Conway.Specification.Fees]: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Conway/Specification/Fees.lagda.md
-[Ledger.Conway.Specification.Gov]: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Conway/Specification/Gov.lagda.md
-[Ledger.Conway.Specification.Rewards]: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Conway/Specification/Rewards.lagda.md
-[Ledger.Conway.Specification.Utxo]: https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/Conway/Specification/Utxo.lagda.md
+[Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md
+[Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
+[Ledger.Properties.PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md
 [LEDGERS]: Ledger.Conway.Specification.Ledger.md#ledgers-transition-system
-[NEWEPOCH]: Ledger.Conway.Specification.Epoch.md#newepoch-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 Declarations]: Ledger.Conway.Specification.PParams.md#protocol-parameter-declarations
+[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
+[The UTXOW Transition System]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system
+[thm:ChainGovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch
 [Time handling on Cardano]: https://docs.cardano.org/about-cardano/explore-more/time
 [Timing of Rewards Payout]: Ledger.Conway.Specification.Rewards.md#sec:timing-of-rewards-payout
-[Type signature of the GOV transition relation]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
-[UTXO]: Ledger.Conway.Specification.Utxo.md#sec:utxo-inference-rule
-[UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:utxos-rule
-[UTXOW]: Ledger.Conway.Specification.Utxow.md#utxow-inference-rules
-[Validity and wellformedness predicates]: Ledger.Conway.Specification.Gov.md#validity-and-wellformedness-predicates
-[Shelley Ledger Spec (pdf)]: https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf
-
-<!-- Properties -->
-[Certs.Properties.PoV]: Ledger.Conway.Specification.Certs.Properties.PoV.md
-[Certs.Properties.PoVLemmas]: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md
-[Chain.Properties.CredDepsEqualDomRwds]: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md
-[Chain.Properties.PParamsWellFormed]: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md
-[Chain.Properties.GovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md
-[Epoch.Properties.GovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md
-[Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md
-[Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
-[Ledger.Properties.PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md
-[lem:EpochGovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md#lem:EpochGovDepsMatch
-[lem:LedgerGovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md#lem:LedgerGovDepsMatch
-[thm:ChainGovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch
+[The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system
+[UTXO]: Ledger.Conway.Specification.Utxo.md#sec:the-utxo-transition-system
 [Utxo.Properties.MinSpend]: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md
 [Utxo.Properties.PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md
-[Gov.Properties.ChangePPGroup]: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md
-[Chain.Properties.EpochStep]: Ledger.Conway.Specification.Chain.Properties.EpochStep.md
-[Epoch.Properties.ConstRwds]: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md
-[Epoch.Properties.NoPropSameDReps]: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md
-[Certs.Properties.VoteDelegsVDeleg]: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.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
 
-[Transactions]: Ledger.Dijkstra.Specification.Transaction.md##sec:transactions
-[Transaction Levels]: Ledger.Dijkstra.Specification.Transaction.md##sec:transaction-levels

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

@@ -82,6 +82,9 @@
             - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
             - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md
         - PoolReap: Ledger.Conway.Specification.PoolReap.md
+        - PoolReap/:
+          - Properties/:
+            - Computational: Ledger.Conway.Specification.PoolReap.Properties.Computational.md
         - PParams: Ledger.Conway.Specification.PParams.md
         - Properties: Ledger.Conway.Specification.Properties.md
         - Ratify: Ledger.Conway.Specification.Ratify.md
@@ -90,6 +93,9 @@
           - Properties/:
             - Computational: Ledger.Conway.Specification.Ratify.Properties.Computational.md
         - Rewards: Ledger.Conway.Specification.Rewards.md
+        - Rewards/:
+          - Properties/:
+            - Computational: Ledger.Conway.Specification.Rewards.Properties.Computational.md
         - RewardUpdate: Ledger.Conway.Specification.RewardUpdate.md
         - RewardUpdate/:
             - Properties: Ledger.Conway.Specification.RewardUpdate.Properties.md
@@ -190,6 +196,20 @@
         - Utxow: Ledger.Conway.Conformance.Utxow.md
         - Utxow/:
           - Properties: Ledger.Conway.Conformance.Utxow.Properties.md
+    - Dijkstra: Ledger.Dijkstra.md
+    - Dijkstra/:
+      - Specification: Ledger.Dijkstra.Specification.md
+      - Abstract: Ledger.Dijkstra.Specification.Abstract.md
+      - Certs: Ledger.Dijkstra.Specification.Certs.md
+      - Gov/:
+        - Actions: Ledger.Dijkstra.Specification.Gov.Actions.md
+        - Base: Ledger.Dijkstra.Specification.Gov.Base.md
+      - PParams: Ledger.Dijkstra.Specification.PParams.md
+      - Script: Ledger.Dijkstra.Specification.Script.md
+      - Script/:
+        - Validation: Ledger.Dijkstra.Specification.Script.Validation.md
+      - TokenAlgebra: Ledger.Dijkstra.Specification.TokenAlgebra.Base.md
+      - Transaction: Ledger.Dijkstra.Specification.Transaction.md
     - PreConway: Ledger.PreConway.md
     - PreConway/:
       - Conformance:
@@ -215,6 +235,7 @@
       - Deriving: Foreign.HaskellTypes.Deriving.md
   - Appendix/:
     - Definitions: Definitions.md
+    - EssentialAgda: EssentialAgda.md
     - Agda Prelude: Prelude.md
     - Type Classes:
       - Interface:

flake.nix

@@ -52,27 +52,32 @@
             ];
           };
 
-          agdaWithPackages = nixpkgs.agda.withPackages (
+          # fls-agda with formal-ledger dependencies
+          fls-agdaWithPackages = nixpkgs.agda.withPackages (
             builtins.filter (p: p ? isAgdaDerivation) nixpkgs.agdaPackages.formal-ledger.buildInputs
           );
 
+          # Override fls-agda in fls-shake to use fls-agda with the formal-ledger dependencies
           fls-shake = inputs.fls-shake.packages.${system}.default.override (_: {
-            fls-agda = agdaWithPackages;
+            fls-agda = fls-agdaWithPackages;
           });
 
+          formal-ledger = nixpkgs.agdaPackages.formal-ledger;
+
+          # Helper to create derivations that reuse _build from formal-ledger
           mkDerivation =
             args:
             let
               default = {
                 version = "0.1";
                 meta = args.meta or { };
                 buildInputs = (args.buildInputs or [ ]) ++ [
-                  agdaWithPackages
+                  formal-ledger
+                  fls-agdaWithPackages
                   fls-shake
-                  nixpkgs.agdaPackages.formal-ledger
                 ];
                 copyAgdaBuild = ''
-                  cp -r "${nixpkgs.agdaPackages.formal-ledger}/_build" .
+                  cp -r "${formal-ledger}/_build" .
                   find _build -type d -print0 | xargs -0 chmod 755
                   find _build -type f -print0 | xargs -0 chmod 644
                 '';
@@ -82,18 +87,27 @@
             nixpkgs.stdenv.mkDerivation (args // default);
 
           pkgs = {
-            formal-ledger = nixpkgs.agdaPackages.formal-ledger;
+            inherit formal-ledger;
             hs-src = nixpkgs.callPackage ./build-tools/nix/hs-src.nix { inherit mkDerivation; };
             html = nixpkgs.callPackage ./build-tools/nix/html.nix { inherit mkDerivation; };
-            mkdocs = nixpkgs.callPackage ./build-tools/nix/mkdocs.nix { inherit mkDerivation; };
+            mkdocs = nixpkgs.callPackage ./build-tools/nix/mkdocs.nix {
+              inherit (nixpkgs.stdenv) mkDerivation;
+              inherit fls-agdaWithPackages;
+            };
           };
         in
         {
+          # ========================
+          # Packages
+          # ========================
           packages = pkgs // {
-            default = pkgs.formal-ledger;
-            inherit agdaWithPackages;
+            default = formal-ledger;
+            inherit fls-agdaWithPackages;
           };
 
+          # ========================
+          # Developer shells
+          # ========================
           devShells = with nixpkgs; {
             default = mkShell {
               inputsFrom = builtins.attrValues pkgs;
@@ -114,10 +128,13 @@
             };
           };
 
+          # ========================
+          # Hydra jobs
+          # ========================
           hydraJobs =
             let
               jobs = {
-                inherit agdaWithPackages;
+                inherit fls-agdaWithPackages;
                 formal-ledger = nixpkgs.agdaPackages.formal-ledger;
               }
               // pkgs;