Home / Input Output / formal-ledger-specifications
Jul 01, 9-10 AM (0)
Jul 01, 10-11 AM (0)
Jul 01, 11-12 PM (0)
Jul 01, 12-1 PM (0)
Jul 01, 1-2 PM (0)
Jul 01, 2-3 PM (0)
Jul 01, 3-4 PM (0)
Jul 01, 4-5 PM (0)
Jul 01, 5-6 PM (0)
Jul 01, 6-7 PM (0)
Jul 01, 7-8 PM (0)
Jul 01, 8-9 PM (1)
Jul 01, 9-10 PM (1)
Jul 01, 10-11 PM (0)
Jul 01, 11-12 AM (0)
Jul 02, 12-1 AM (0)
Jul 02, 1-2 AM (0)
Jul 02, 2-3 AM (0)
Jul 02, 3-4 AM (0)
Jul 02, 4-5 AM (0)
Jul 02, 5-6 AM (4)
Jul 02, 6-7 AM (0)
Jul 02, 7-8 AM (0)
Jul 02, 8-9 AM (0)
Jul 02, 9-10 AM (0)
Jul 02, 10-11 AM (0)
Jul 02, 11-12 PM (0)
Jul 02, 12-1 PM (3)
Jul 02, 1-2 PM (1)
Jul 02, 2-3 PM (0)
Jul 02, 3-4 PM (0)
Jul 02, 4-5 PM (0)
Jul 02, 5-6 PM (0)
Jul 02, 6-7 PM (0)
Jul 02, 7-8 PM (0)
Jul 02, 8-9 PM (0)
Jul 02, 9-10 PM (0)
Jul 02, 10-11 PM (0)
Jul 02, 11-12 AM (0)
Jul 03, 12-1 AM (1)
Jul 03, 1-2 AM (0)
Jul 03, 2-3 AM (0)
Jul 03, 3-4 AM (0)
Jul 03, 4-5 AM (0)
Jul 03, 5-6 AM (0)
Jul 03, 6-7 AM (0)
Jul 03, 7-8 AM (0)
Jul 03, 8-9 AM (1)
Jul 03, 9-10 AM (2)
Jul 03, 10-11 AM (2)
Jul 03, 11-12 PM (2)
Jul 03, 12-1 PM (2)
Jul 03, 1-2 PM (0)
Jul 03, 2-3 PM (0)
Jul 03, 3-4 PM (0)
Jul 03, 4-5 PM (0)
Jul 03, 5-6 PM (0)
Jul 03, 6-7 PM (0)
Jul 03, 7-8 PM (1)
Jul 03, 8-9 PM (0)
Jul 03, 9-10 PM (0)
Jul 03, 10-11 PM (0)
Jul 03, 11-12 AM (0)
Jul 04, 12-1 AM (0)
Jul 04, 1-2 AM (0)
Jul 04, 2-3 AM (0)
Jul 04, 3-4 AM (2)
Jul 04, 4-5 AM (0)
Jul 04, 5-6 AM (0)
Jul 04, 6-7 AM (0)
Jul 04, 7-8 AM (0)
Jul 04, 8-9 AM (0)
Jul 04, 9-10 AM (0)
Jul 04, 10-11 AM (0)
Jul 04, 11-12 PM (0)
Jul 04, 12-1 PM (0)
Jul 04, 1-2 PM (0)
Jul 04, 2-3 PM (0)
Jul 04, 3-4 PM (0)
Jul 04, 4-5 PM (0)
Jul 04, 5-6 PM (0)
Jul 04, 6-7 PM (0)
Jul 04, 7-8 PM (0)
Jul 04, 8-9 PM (0)
Jul 04, 9-10 PM (0)
Jul 04, 10-11 PM (0)
Jul 04, 11-12 AM (0)
Jul 05, 12-1 AM (0)
Jul 05, 1-2 AM (0)
Jul 05, 2-3 AM (1)
Jul 05, 3-4 AM (0)
Jul 05, 4-5 AM (0)
Jul 05, 5-6 AM (0)
Jul 05, 6-7 AM (0)
Jul 05, 7-8 AM (0)
Jul 05, 8-9 AM (0)
Jul 05, 9-10 AM (0)
Jul 05, 10-11 AM (0)
Jul 05, 11-12 PM (0)
Jul 05, 12-1 PM (0)
Jul 05, 1-2 PM (0)
Jul 05, 2-3 PM (0)
Jul 05, 3-4 PM (0)
Jul 05, 4-5 PM (0)
Jul 05, 5-6 PM (0)
Jul 05, 6-7 PM (0)
Jul 05, 7-8 PM (0)
Jul 05, 8-9 PM (0)
Jul 05, 9-10 PM (0)
Jul 05, 10-11 PM (0)
Jul 05, 11-12 AM (0)
Jul 06, 12-1 AM (0)
Jul 06, 1-2 AM (0)
Jul 06, 2-3 AM (0)
Jul 06, 3-4 AM (0)
Jul 06, 4-5 AM (0)
Jul 06, 5-6 AM (0)
Jul 06, 6-7 AM (0)
Jul 06, 7-8 AM (0)
Jul 06, 8-9 AM (0)
Jul 06, 9-10 AM (0)
Jul 06, 10-11 AM (0)
Jul 06, 11-12 PM (0)
Jul 06, 12-1 PM (0)
Jul 06, 1-2 PM (0)
Jul 06, 2-3 PM (0)
Jul 06, 3-4 PM (0)
Jul 06, 4-5 PM (0)
Jul 06, 5-6 PM (0)
Jul 06, 6-7 PM (0)
Jul 06, 7-8 PM (0)
Jul 06, 8-9 PM (0)
Jul 06, 9-10 PM (0)
Jul 06, 10-11 PM (0)
Jul 06, 11-12 AM (0)
Jul 07, 12-1 AM (1)
Jul 07, 1-2 AM (0)
Jul 07, 2-3 AM (1)
Jul 07, 3-4 AM (0)
Jul 07, 4-5 AM (0)
Jul 07, 5-6 AM (0)
Jul 07, 6-7 AM (0)
Jul 07, 7-8 AM (1)
Jul 07, 8-9 AM (0)
Jul 07, 9-10 AM (0)
Jul 07, 10-11 AM (0)
Jul 07, 11-12 PM (0)
Jul 07, 12-1 PM (0)
Jul 07, 1-2 PM (1)
Jul 07, 2-3 PM (0)
Jul 07, 3-4 PM (1)
Jul 07, 4-5 PM (0)
Jul 07, 5-6 PM (0)
Jul 07, 6-7 PM (2)
Jul 07, 7-8 PM (0)
Jul 07, 8-9 PM (0)
Jul 07, 9-10 PM (0)
Jul 07, 10-11 PM (0)
Jul 07, 11-12 AM (0)
Jul 08, 12-1 AM (0)
Jul 08, 1-2 AM (0)
Jul 08, 2-3 AM (0)
Jul 08, 3-4 AM (0)
Jul 08, 4-5 AM (0)
Jul 08, 5-6 AM (0)
Jul 08, 6-7 AM (2)
Jul 08, 7-8 AM (0)
Jul 08, 8-9 AM (0)
Jul 08, 9-10 AM (0)
33 commits this week Jul 01, 2025 - Jul 08, 2025
Improve migration pipeline and begin migration (#805)
+  begin migration with rename

+  migrate Introduction.lagda

+  major refactoring of pipeline scripts

   This new functional version provides

   1. Atomicity: each operation either succeeds completely or fails cleanly;
   2. Composability: functions can be combined mathematically using `and_then`;
   3. Testability: each function can be tested in isolation;
   4. Error Transparency: all possible failure modes are explicit in the type system;
   5. Immutability: no hidden state changes or side effects.

+  refactor: factor out latex processing module

   + 🎯 Pure Transformations: each stage is a function
   + 🔒 Immutable Types: `LaTeXProcessingStage`, `LaTeXProcessingResult`
   + ⚡ Functional Composition: chainable with monadic error handling
   + 🗺️ Label Resolution: extracts cross-references for global mapping
   + 🔄 Result Monad: all operations wrapped in `Result<T, PipelineError>`

+  add bibtex handling and fix docs of build.py

   1. New Bibliography Processing Stage
      - `run_bibliography_stage()` function uses `process_bibliography_stage()`
      - graceful fallback if bibliography processing unavailable

   2. Split Postprocessing
      - `run_postprocess_stage()` now outputs to intermediate `postprocess_file`
      - bibliography stage takes this as input and produces final `.lagda.md`

   3. Enhanced Data Structure
      - Added `postprocess_file: Path` to `LaTeXProcessingStage` for the intermediate file between postprocessing and bibliography

   4. **Complete 6-Stage Pipeline**:
      1. Preprocessing: `.lagda` → `.lagda.temp` + `code_blocks.json`
      2. Label Map Generation: Extract cross-references from temp files
      3. Pandoc + Lua: `.lagda.temp` → `.md.intermediate`
      4. Postprocessing: `.md.intermediate` → `.md.postprocess`
      5. Bibliography: `.md.postprocess` → `.lagda.md` (with citations)
      6. Cleanup: Remove original `.lagda` files

+  Update src/Ledger/Introduction.lagda.md

+  Merge functionality into new module

   1.  New Module: `modules/asset_generator.py` contains core functions for generating `macros.json` and `custom.css`.
   2.  Updated `build.py`:
         * It now imports `generate_macros_json` and `generate_custom_css_from_agda` from the new module.
         * The old `macros_path` helper function has been replaced with `generate_and_save_macros_json`, which calls the imported function directly instead of using `subprocess`.
         * The old `generate_custom_css_from_agda` and `generate_and_deploy_css` helpers have been replaced by a single, cleaner function `generate_and_deploy_custom_css` that uses the new module.

+  consolidate Agda-specific logic; clarify role of LaTeX preprocessor

+  factor out `run_command` into new module

+  restore Agda type-checking output using stream

+  simplify main build script

   + remove top-level path constants and instead
   + load configuration once in `main` and pass `config` object to functions that need path info
   + remove unused `LagdaProcessingPaths` helper class (no longer being used anywhere)

+  pass nixfmt formatter

+  add required/nonrequired jobs to CI

+  fix CI

+  factor more functionality out of build.py

   +  `build-tools/scripts/md/modules/site_assembly.py`
      handles all final steps: copying staged content, deploying all assets (CSS, JS, BibTeX), and generating the final `mkdocs.yml`.

   +  `build-tools/scripts/md/modules/content_staging.py`
      prepares the processed markdown files for the site assembly step.

+  remove html from ci and fix bottom of intro

+  Clean up project structure, remove dead code, and group related functions more logically without changing the pipeline's overall behavior.

   This refactoring replaces large, imperative `try-except` blocks with collections of
   smaller, pure, testable functions composed in a robust chain. It's a significant
   improvement in the clarity and reliability of the Agda processing stage.

   +  Functions in `modules/` orchestrate the pipeline logic. They describe *what* to do
   and should be free of `try-except` blocks for I/O. They operate on `Result` objects.

   +  Functions in `utils/` provide reusable tools that perform the "impure" work. They
      are the "boundary" and use `try-except` internally to convert exceptions into `Err`
      values.

   +  Move pure logic to utility modules.

   +  All functions in `postprocess.py` that perform text replacements are pure
      transformations; move them to `utils/text_processing.py`, making them reusable
      utilities. To make them truly pure, modified them to accept data (like code
      blocks and label maps) as arguments instead of relying on global variables.

   +  Update Pipeline Orchestrator. Add new function to `modules/latex_pipeline.py` that
      orchestrates these post-processing steps.  Replaces old method of calling
      `postprocess.py` as an external script, which eliminates a `subprocess` call and
      integrates the logic seamlessly.

   +  Delete Legacy Script. `postprocess.py` is now retired.

   +  Add new `utils/file_ops.py` utility module including directory functions from `setup.py`.

   +  Merge `asset_generator.py` into `site_assembly.py`, since `site_assembly.py`
      already uses functions from `asset_generator.py`. 

   +  Clean up `build_config.py` (remove `get_legacy_paths()`---it's now dead code)

   +  Error handling is now more precise: it skips files that are missing their
      intermediate parts (a recoverable issue) but will correctly halt the entire build on
      a more serious problem (like a permissions error when writing the final file).

   +  More specific exceptions. The functions now catch `OSError` for file system
      permission issues, which is more descriptive than a generic `Exception`.

   +  Cleaner Logic. functions are now simpler and no longer returns a `Result`, as a
      `FileNotFoundError` is not a critical failure for this specific task—it simply means
      the file size is 0.

      1.  Correct Usage (Boundary Functions).

          The `try` blocks in `utils/command_runner.py` and `utils/file_ops.py` are
          fine; they serve as the necessary bridge between impure libraries
          (`subprocess`, `shutil`) and our functional code. These should stay.

      2.  Candidates for Refactoring (Orchestration Logic).

          Most other `try` blocks, especially those in the `modules/` directory, are
          wrapping larger chunks of logic. These are prime candidates for refactoring.
          Instead of a large `try...except` block, these functions should be chains of
          smaller operations that each return a `Result`.

   +  No `try-except`. The main logic is now free of explicit exception handling. All
      I/O error handling is delegated to the `ls_dir` utility.

   +  Clarifies Error Handling.  The `calculate_file_metadata` function remains a good
      example of a case where a local `try-except` is a valid choice because the goal is
      to **provide a default value**, not to halt the entire pipeline on failure. This
      distinguishes it from critical I/O operations where failure must be propagated.

   +  Declarative. The code now reads like a description of what it does ("list the
      directory and then map the result to processed files") rather than a sequence of
      imperative steps.

   +  Preserves Behavior. Because our `calculate_file_metadata` function already handles
      its own `FileNotFoundError` by returning a default value, the mapping operation
      `[... for p in paths]` is safe and won't crash the whole pipeline if one file has
      an issue, perfectly preserving the logic of your original implementation.

+  add footnotes extension and fix admonitions

+  bugfix: caption-to-subsection label conversion

+  fix nav template

+  Create References section

   1.  **Removed LaTeX Logic**

       All the code related to `if config.output_format == "latex":` has been
       removed. The function's single responsibility is now to generate Markdown.

   2.  **Fixed Anchor Syntax**

       The problematic `{#...}` syntax is replaced with `<span
       id="{entry.key}"></span>`. This creates a standard HTML anchor that works
       reliably in all Markdown renderers and will not appear as visible text.

   3.  **Fixed Italics**

       The call to `format_bibliography_entry` now explicitly passes
       `output_format="markdown"`, ensuring it uses asterisks (`*...*`) for italics,
       as intended for the final Markdown page.

+  improve bibtex citation handling

---------

Co-authored-by: William DeMeo <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: Carlos Tomé Cortiñas <[email protected]>