Merge branch 'master' into carlos/refactor-feesOK
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
Merge branch 'master' into carlos/make-txdats-a-set
Artifacts generated from 6bd4ffadc9caff0fc850b0bc865c247f414d5e7a
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]>
Artifacts generated from 8a2cdc293b456132d9eebd585374c47106225f2e
Inline minfee check; refactor collateral check to collateralCheck function
Inline scriptsNeeded and vKeysNeeded
final improvements
improve bibtex citation handling
fix nav template
Artifacts generated from 50f9fa62a1fa87b57f88509299fad6c7b498512b
address change requests
add footnotes extension and fix admonitions
Artifacts generated from a53e698191f2ddd8aa77cbc0857043832c76f727
Rename collectP2Scripts to collectP2ScriptsWithContext (to align with cardano-ledger)
Start cleaning ScriptVerification
Artifacts generated from a6a04408c53763d3a2f2474f78b58b528547c1bc
Artifacts generated from 0e6280b12957abd9c51aca50c8d11d66205a3291
Refactor getInputHashes and getDataHashes; rename premises in UTxOw
Artifacts generated from 89aaf46c5c1577d61294f00851c96aa718624bae
Artifacts generated from aaa3fc4d9aa57093adfb09001cda60a277b201a6
Artifacts generated from cfc380b6f7ce202c22f69c83eadc1eab67f90fc5
Clean Script.Validation