merge master into dijkstra-dev #937
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
+ add derivation for markdown pipeline
+ initial commit of scripts for md pipeline
+ fix broken derivation (wrong nixpkgs version)
+ fix CI: replace `nix-shell` with `nix develop`
+ update and improve md_build.py master script and doc comments
**Summary of Key Changes:**
1. **Logging Added:** Replaced `print(..., file=sys.stderr)` with standard Python `logging` directed to both console (INFO level) and a file (`_build/docs/build.log`, DEBUG level).
2. **Snapshot Directory:** Added `AGDA_SNAPSHOT_SRC_DIR` variable.
3. **Source Copy:** Added `shutil.copytree` to copy the entire `src/` directory to `AGDA_SNAPSHOT_SRC_DIR` at the beginning.
4. **Loop Modification:** Inside the loop, after `postprocess.py` creates `current_final_lagda_md`, added `shutil.copy2` to copy this generated file into the correct relative path within `AGDA_SNAPSHOT_SRC_DIR`.
5. **`agda --html` Removed:** The `run_command` call for `agda --html` is removed from this script.
6. **MkDocs Assembly (Optional Preview):** Kept the logic to assemble an MkDocs site source (`MKDOCS_SRC_DIR`), but it now copies the intermediate `current_final_lagda_md` files into `MKDOCS_DOCS_DIR`. This site *will not* have the Agda HTML highlighting but can be used to preview the Markdown conversion and structure. Removed `Agda.css` from its default `mkdocs.yml` config.
7. **Final Messages:** Updated the completion messages to point to `AGDA_SNAPSHOT_SRC_DIR` as the main output for the next (Shake) step and the `MKDOCS_SRC_DIR` as an optional preview site.
+ improve md_build script
**Summary of Key Changes:**
1. **Logging Added:** Imports `logging`, calls `setup_logging()` at the start of `main()`, replaces `print(..., file=sys.stderr)` with standard Python logging calls (`logging.info`, `logging.warning`, `logging.error`, `logging.debug`) directed to both console (INFO level) and a file (`_build/docs/build.log`, DEBUG level). Adds `logging.shutdown()` at the end.
2. **Snapshot Directory:** Creates `AGDA_SNAPSHOT_SRC_DIR`.
3. **Source Copy:** Copies `SRC_DIR` to `AGDA_SNAPSHOT_SRC_DIR` using `shutil.copytree`.
4. **`.agda-lib` Generation:** Creates a basic `snapshot.agda-lib` file inside `AGDA_SNAPSHOT_SRC_DIR`. **You will need to customize the `depend:` list** in the `agda_lib_content` string to match your project's actual library dependencies.
5. **Loop Modification:**
* After `postprocess.py` runs (creating `current_final_lagda_md`), it deletes the original `.lagda` file from the snapshot (`snapshot_original_lagda.unlink()`).
* It then copies `current_final_lagda_md` to the snapshot directory (`snapshot_target_path`).
6. **Optional `agda --html` Step:**
* Added an `--run-agda` command-line flag using `argparse`.
* The `agda --html` step (inside the loop) is wrapped in `if run_agda_html:`.
* The command now runs with `cwd=AGDA_SNAPSHOT_SRC_DIR.resolve()` and uses `-i .` relative to that directory.
* Added basic error handling for the Agda command and fallback logic (copying the `.lagda.md` file if Agda fails).
7. **Conditional MkDocs Assembly:**
* The step copying files to `MKDOCS_DOCS_DIR` now conditionally copies either the Agda HTML output (`*.md`) or the intermediate (`*.lagda.md`) files based on the `--run-agda` flag.
* It conditionally adds `Agda.css` to `mkdocs.yml` only if the Agda step ran successfully.
8. **Robustness:** Added more specific error handling, path resolutions, existence checks, and more informative logging messages.
+ improve md_build.py script
**Summary of Key Changes**
+ *Logging Added*: Replaced print(..., file=sys.stderr) with standard Python logging directed to both console (INFO level) and a file (_build/docs/build.log, DEBUG level). Added logging.shutdown() at the end.
+ *Snapshot Directory*: Creates AGDA_SNAPSHOT_SRC_DIR.
+ *Source Copy*: Copies SRC_DIR to AGDA_SNAPSHOT_SRC_DIR using shutil.copytree.
+ *.agda-lib Generation*: Creates a basic snapshot.agda-lib file inside AGDA_SNAPSHOT_SRC_DIR. You will need to customize the depend: list in the agda_lib_content string to match your project's actual library dependencies.
+ *Loop Modification*:
+ After postprocess.py runs (creating current_final_lagda_md), it deletes the original .lagda file from the snapshot (snapshot_original_lagda.unlink()).
+ It then copies current_final_lagda_md to the snapshot directory (snapshot_target_path).
+ *Optional agda --html Step*:
+ Added an --run-agda command-line flag using argparse.
+ The agda --html step (inside the loop) is wrapped in if run_agda_html:.
+ The command now runs with cwd=AGDA_SNAPSHOT_SRC_DIR.resolve() and uses -i . relative to that directory.
+ Added basic error handling for the Agda command and fallback logic (copying the .lagda.md file if Agda fails).
+ *Conditional MkDocs Assembly*:
+ The step copying files to MKDOCS_DOCS_DIR now conditionally copies either the Agda HTML output (*.md) or the intermediate (*.lagda.md) files based on the --run-agda flag.
+ It conditionally adds Agda.css to mkdocs.yml only if the Agda step ran successfully.
+ *Robustness*: Added more specific error handling, path resolutions using pathlib.resolve(), existence checks, improved logging messages, and used shutil.copy2 to preserve metadata. Refined YAML loading and nav generation slightly.
+ improve shell.nix
+ add `let` binding named `pythonEnv`
+ `pkgs.python311.withPackages (ps: [ ... ])` creates a derivation for
Python 3.11 environment needed for markdown migration scripts and mkdocs
site build.
+ In `markdownDocsShell`'s `nativeBuildInputs`, replaced individual Python
packages (`pkgs.python311`, `pkgs.python311Packages.*`) with `pythonEnv`
derivation, making Python interpreter and associated packages available correctly.
+ improve master build script
**Summary of Changes:**
1. **In the `--run-agda` section:**
* Calculate the `target_path_relative_to_mkdocs_docs` to ensure it ends with `.md` and reflects the desired subdirectory structure (e.g., `Ledger/File.md`).
* Calculate `agda_html_source_file` based on the Agda module name (e.g., `Ledger.File.md`) inside `AGDA_HTML_OUTPUT_DIR`.
* Copy from `agda_html_source_file` to `MKDOCS_DOCS_DIR / target_path_relative_to_mkdocs_docs`.
* Append `str(target_path_relative_to_mkdocs_docs)` to `final_md_files_for_mkdocs`.
2. **In the `else` (no Agda) section:**
* Ensure the copied files are renamed from `.lagda.md` to `.md` in the `mkdocs_src/docs` directory.
* Append the correct relative `.md` path to `final_md_files_for_mkdocs`.
3. **Navigation Generation:**
* Introduce the `build_nested_nav` helper function.
* Use this function to generate `mkdocs_config['nav']` from the `final_md_files_for_mkdocs` list.
**Key changes in revised function**
1. **Improved Node Traversal/Creation:**
* `next_level_node = current_level_dict.get(title_part)` fetches the potential next level.
* If it's already a `dict`, we traverse into it.
* If it's `None` (doesn't exist), we create it as a new `dict`.
* If it exists but is *not* a `dict` (i.e., it's a string/file path from a previous step), we log a warning and overwrite it with a `dict` to "promote" it to a section. This resolves the `TypeError`.
2. **Conflict Handling for Files vs. Sections:**
* Added a check before assigning the `file_path_str`: If a dictionary (section) already exists with the `file_title`, it logs a warning. This prevents a file from silently overwriting a whole section in the `nav_tree` or vice-versa. We might want a different strategy here (e.g., creating an `index.md` equivalent or a specially named entry).
+ reorganization to reflect feedback from Carlos
+ commit new script to convert all to literate agda
+ adjust agda2lagda for calling from build.py
+ add `project_root_for_logging` parameter to control base path for relative logging;
+ return `True` for overall success, `False` if any critical error occurred;
+ includes an `if __name__ == '__main__':` block so it can be run directly from cli;
+ set up basic logging and include user prompts and confirmation.
+ improve literate agda conversion itegration
+ improve master build script
**Key Changes in `main` function and new `LagdaProcessingPaths` class**
1. **`LagdaProcessingPaths` Class**
+ new class that takes a `relative_path` (e.g., `Path("Module/File.lagda")`) as input;
+ immediately constructs all necessary `current_...` paths based on given `relative_path` and global config paths
(e.g., `TEMP_DIR`, `FINAL_LAGDA_MD_DIR`, `AGDA_SNAPSHOT_SRC_DIR`, etc.);
+ has `ensure_parent_dirs_exist()` method to create all necessary output subdirectories for the specific file.
2. **Simplified Loop in `main`**
+ inside loop `for lagda_file_abs_path in original_lagda_files:`, first do
```python
relative_path = lagda_file_abs_path.relative_to(SRC_DIR)
paths = LagdaProcessingPaths(relative_path)
paths.ensure_parent_dirs_exist()
```
+ then all subsequent path refs use `paths.temp_lagda`, `paths.final_lagda_md`,
`paths.snapshot_target_lagda_md`, etc, making logic cleaner and doesn't redefine
similar paths repeatedly.
3. **Logic for `processed_literate_files_in_snapshot`**
+ how `processed_literate_files_in_snapshot` is populated is changed:
+ initialize by finding all existing `.lagda.md` files in `AGDA_SNAPSHOT_SRC_DIR`
(the ones converted from `.agda`);
+ as each original `.lagda` file is processed by pipeline and output `.lagda.md`
is copied to the snapshot, that snapshot path is also added to this list.
+ Before `agda --html` step,
`unique_processed_snapshot_files = sorted(list(set(processed_literate_files_in_snapshot)))`
ensures clean, unique, and sorted list to iterate over, making build more deterministic,
avoiding processing same file twice if overlaps exist.
4. **Clarity in `agda --html` step**
+ path manipulations and logging in `agda --html` section made more explicit, deriving
paths from `lagda_md_in_snapshot` (an absolute path to a file in `AGDA_SNAPSHOT_SRC_DIR`);
+ Agda module name calculation is clarified;
+ input file to `agda --html` command is now `str(relative_path_in_snapshot)` because CWD
for Agda command is `AGDA_SNAPSHOT_SRC_DIR.resolve()`.
5. **`final_md_files_for_mkdocs` population**
+ list now consistently populated with paths *relative to `MKDOCS_DOCS_DIR`* and always
with `.md` suffix, regardless of whether the Agda HTML step ran or if it was a
fallback---crucial for `build_nested_nav` function.
6. **MkDocs `index.md` and Navigation**
+ logic for handling `index.md` (copying from template, creating minimal one if missing) and
ensuring it's part of `final_md_files_for_mkdocs` for navigation is refined for robustness;
+ `final_md_files_for_mkdocs` explicitly sorted with `index.md` before calling `build_nested_nav`.
7. **`mkdocs.yml` generation**
+ improved merging logic for `mkdocs.yml` when template is present, especially for list-based
configurations like `extra_css`, `extra_javascript`, and `markdown_extensions` to ensure
defaults are appended if not already covered by template;
+ path logging made more consistent with `relative_to(PROJECT_ROOT)`.
+ remove emoji package options breaking mkdocs
+ improve build.py and lua script
(description of changes are in the comments of build.py)
+ add/fix cleanup function; revise documentation
+ improve master build script
The `run_command` for Agda is now called only once on
`CardanoLedger.lagda.md`; the idea is that this will generate html for
all of `CardanoLedger.lagda.md`'s dependencies.
+ improve/debug build.py
removing cleanup step for now while debugging
+ preprocess now handles figure captions and labels
+ improve handling of fig captions, labels, and refs
+ improve build and postprocess scripts
+ fix some bugs
+ attempt better handling of fig caption and labels
+ fixed caption -> heading bug
line breaks of captions were being preserved which was causing incorrect subsection headings
+ fix links in fls Agda code
+ fix links in built-ins (with html-based pages)
+ cleanup and improvements
+ add support for optional static content
+ revise documentation
+ Update scripts/mkdocs/postprocess.py
Co-authored-by: Copilot <[email protected]>
+ reorganize to reflect Carlos' suggestions
Also, add documentation explaining purposes of the `mdsrc` and `mkdocs` directories.
+ adjust build.py to new directory structure
+ rm unnecessary packages in markdown nix derivation
---------
Co-authored-by: William DeMeo <[email protected]>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: William DeMeo <[email protected]>
* Add `flowConservation` to `RewardUpdate` * Add inequalities `0 ≤ Δt` and `Δf ≤ 0` to `RewardUpdate` --------- Co-authored-by: William DeMeo <[email protected]>
* Add agda-fls backend * Reorganize repo * Rename lib-exts to src-lib-exts * Fix shell.nix * Fix gh action * Merge shell.nix into default.nix * Refactor flake.nix * Add agda and fls-shake to Hydra * Refactor default.nix * Add customHtml to mkMd; add stdlib as a niv source * Port agda deps. to use niv * Restrict systems it builds to x86_64 * Rename agdaLibs to snake-case; clean backend; fix nix stuff * Add nix agda infra * update CONTRIBUTING.md with Nix config notes * Apply suggestions from code review * Unbundle fls-shake nix set * Remove unused derivation * Rename mkDocsDerivation to mkPdfDerivation --------- Co-authored-by: William DeMeo <[email protected]>
* major refactoring to make build script generic ...so it's easier to integrate different static website builders. In particular, I'm in the process of making the script build both mkdocs and mdbook sites. --------- Co-authored-by: William DeMeo <[email protected]> Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
* Add option to fls-agda backend to generate HTML for the main file only * Add AgdaKaTeX to mkdocs * Fix CI --------- Co-authored-by: William DeMeo <[email protected]>
* Add formalLedger as a buildInput * Inherit all derivations * Add custom mkDerivation * Add project to package name for pdfs * Update name of target in gh action * Rename hsSrc (for consistency) * Remove build-support; format * Uncomment section; fix imports * Add mkdocs derivation; use it in gh action * Fix CI * Update README
* Rearrange module structure for scripts and token algebra
* Move Tactic.{Derive.DecEq,Inline} to Ledger.Prelude
* Fix mkdocs in CI
+ 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]>
* Refactor functionality related to scripts
+ Move `credsNeeded` to ScriptValidation
+ Refactor `getDatum`
+ Rename premises in UTxOw
* Move ScriptValidation to Script.Validation
* Clean Script.Validation
* Rename and refactor collectPhaseTwoScripts
* Rename collectP2Scripts inputs to collectP2Scripts; evalScripts to evalP2Scripts
* Refactor getInputHashes and getDataHashes; rename premises in UTxOw
* Start cleaning ScriptVerification
* Rename collectP2Scripts to collectP2ScriptsWithContext (to align with cardano-ledger)
* Trigger Hydra
* Revert "Start cleaning ScriptVerification"
This reverts commit 1076e8a.
* Uncomment leftover code
* Inline scriptsNeeded and vKeysNeeded
---------
Co-authored-by: William DeMeo <[email protected]>
* Add hook to mkdocs to use html comments for hidden code * Use comments in Introduction.lagda.md --------- Co-authored-by: William DeMeo <[email protected]>
* Move GovernanceActions to Governance.Actions * Move Types.GovStructure to Governance.Base * Unify Governance and Gov folders * Move ChangePPGroup to Gov
* Remove dep. on Conformance * Add --safe flag to Script Verification modules * Move Script verification to Ledger.Conway.Test
Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
Combined multiple small commits that fine-tuned markdown formatting, fixed broken links, and applied final polish to HTML/CI-related setup; add icons for fun; other improvements.
Grouped multiple commits that cleaned up internal/external links, nav paths, and log output redundancies.
* Fix broken link in Fees.lagda.md This closes issue #893 Just to be sure, add redundant/backup link definition to links.md. Also removed unused html id ref. * fix another broken link * restore anchor lost during migration * Update src/Ledger/Conway/Specification/Epoch.lagda.md
replace tex with md and fix links
code refinements and formatting improvements retire hiding of `data` convention; other improvements
Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
(Somehow it got renamed and committed as `tmp` in my last PR.)
And add `*.orig` to `.gitignore` so hopefully this doesn't happen again!
* Remove mdbook * fix some issues In particular, we need to keep the js path in the build_config, otherwise we won't have the nice colors in dark mode. Also, I think we should either continue to have an `md/common` (and put there everything that could be used in other web platforms) OR put everything under `md/mkdocs/docs` (e.g., `css/custom.css` and `js/custom.js`), but I don't think we should have an `md/common` that only contains just *some* of the common stuff. * we no longer need custom_js_path but we do need md_js_dir (for katex-config.js) --------- Co-authored-by: William DeMeo <[email protected]>
and fix resulting issues in Ledger.Properties
And make sure Ledger/Properties/Computational.lagda doesn't result in a blank page (without "Show more Agda").
This is a first step to refactoring the CERTS rule. Ultimately we will deprecate the "CERTBASE" rule and replace it with "preCerts" and "postCerts" functions that will run before and after the CERTS sts. Some of the things that currently happen in CERTBASE may be moved into the LEDGER rule. revert CERTS rule in conformance version
Plus, + computational proofs for new pre-cert and post-cert rules + PoV proofs for new CERTS rule + Refactor equivalence proofs for new CERTS rule. + fix some formatting in Ledger module Also, removed `AgdaInductiveConstructor` class from occurrences of "DRep" in the text; this makes it easier to be consistent throughout the document, but even if we do want to use Agda high-lighting for "DRep", it's not clear to me that `AgdaInductiveConstructor` is the right class to use.
and fix bug introduced by rebase
Member
Author
|
Unnecessary. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
Making this big merge a PR, just to be safe.
Checklist
CHANGELOG.md