Skip to content

Migrate all remaining lagda files #945

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
williamdemeo merged 13 commits into from
Oct 26, 2025
Merged

Migrate all remaining lagda files #945

williamdemeo merged 13 commits into from
Oct 26, 2025

Conversation

@williamdemeo
Copy link
Member

@williamdemeo williamdemeo commented Oct 8, 2025 •
edited
Loading

Description

Closes issue #944.

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • Any semantic changes to the specifications are documented in CHANGELOG.md
  • Code is formatted according to CONTRIBUTING.md
  • Self-reviewed the diff

@williamdemeo williamdemeo linked an issue Oct 8, 2025 that may be closed by this pull request
Migrate all remaining .lagda files #944
Closed
@williamdemeo williamdemeo force-pushed the 944-migrate-all-remaining-lagda-files branch 2 times, most recently from 2d7ab59 to bae4713 Compare October 9, 2025 04:44
@williamdemeo williamdemeo marked this pull request as ready for review October 10, 2025 05:22
carlostome
carlostome reviewed Oct 10, 2025
View reviewed changes
Copy link
Collaborator

@carlostome carlostome left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good. I left some comments here and there.

I think this PR should also migrate NEWEPOCH.

@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 14, 2025

@carlostome I'm not sure what you mean by, "I think this PR should also migrate NEWEPOCH."

@williamdemeo williamdemeo force-pushed the 944-migrate-all-remaining-lagda-files branch from 5eb42b9 to 5a2ff27 Compare October 16, 2025 04:09
carlostome
carlostome requested changes Oct 16, 2025
View reviewed changes
Copy link
Collaborator

@carlostome carlostome left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks nice, I think It's getting in shape! I left some more comments here and there.

src/Ledger/Conway/Specification/Ratify.lagda.md
on current proposals, re-evaluate existing proposals with respect to a
new constitution, and ensures that the (in principle arbitrary) semantic
changes caused by enacting a hard-fork do not have unintended
consequences in combination with other actions.
Copy link
Collaborator

@carlostome carlostome Oct 16, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This paragraph is too informal for a specification. I think it needs a pass.

In addition the type and auxiliary functions of Delaying actions are defined. Maybe this text should be closer to that.

Copy link
Member Author

@williamdemeo williamdemeo Oct 17, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good. Although, there is certainly room in the prose of the formal specification for less formal, more heuristic explanations. I suppose as long as it's made precise somewhere... but in some instances that "somewhere" may be the Agda formalization itself. Of course, if the Agda code is ambiguous, that is a problem!

Copy link
Member Author

@williamdemeo williamdemeo Oct 17, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, I'm not exactly sure what you mean by "a pass." Do you mean it should be revised? Or do you mean we should "pass on it," as in delete it?

@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 17, 2025

@carlostome Thank you for the detailed review! I think it should be good to go now.

@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 17, 2025

Before merging this we should make sure all .agda files are also migrated to .lagda so that artifacts don't have to be rebuilt.

@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 19, 2025

@carlostome it seems the mkdocs flake derivation (nix develop #.mkdocs) now builds the whole ledger (formal-ledger-0.1), which type-checks everything. Is that intentional? I think we should avoid this and instead type-check everything when we build the mkdocs site with the python command, no?

@carlostome
Copy link
Collaborator

carlostome commented Oct 20, 2025

@carlostome it seems the mkdocs flake derivation (nix develop #.mkdocs) now builds the whole ledger (formal-ledger-0.1), which type-checks everything. Is that intentional? I think we should avoid this and instead type-check everything when we build the mkdocs site with the python command, no?

It was not intentional. I have fixed this in the latests commits

@williamdemeo williamdemeo force-pushed the 944-migrate-all-remaining-lagda-files branch from 8bfe784 to fdbe355 Compare October 20, 2025 20:01
@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 20, 2025

@carlostome you mentioned that we should make it so that Conformance and Foreign are not part of the mkdocs site. I think we should make that a separate issue/PR (separate from this PR).

@carlostome carlostome force-pushed the 944-migrate-all-remaining-lagda-files branch from 4ec9480 to c9b6ba1 Compare October 22, 2025 14:22
carlostome
carlostome reviewed Oct 23, 2025
View reviewed changes
@williamdemeo
Copy link
Member Author

williamdemeo commented Oct 24, 2025

@carlostome I think this is ready to be merged :octocat:

carlostome
carlostome approved these changes Oct 24, 2025
View reviewed changes
Copy link
Collaborator

@carlostome carlostome left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, Nice work!

williamdemeo and others added 8 commits October 24, 2025 14:51
@williamdemeo
prepare to migrate the following:
7d87560 
+ `EssentialAgda.lagda{,.md}`
+ `Utxow.lagda{,.md}`
+ `Actions.lagda{,.md}`
+ `Properties.lagda{,.md}`
+ `Chain.lagda{,.md}`
+ `Ledger.Properties.Computational.lagda{,.md}`
+ `Test.StructuredContracts.lagda{,.md}`
+ `Ratify.lagda{,.md}`
+ `PParams.lagda{,.md}`
+ `Address.lagda{,.md}`
+ `Crypto.lagda{,.md}`
+ `TokenAlgebra.Base.lagda{,.md}`
+ `TokenAlgebra.ValueSet.lagda{,.md}`
+ `PreConway` files
@williamdemeo
migrate the following:
87b9e0f 
+ `EssentialAgda.lagda{,.md}`
+ `Utxow.lagda{,.md}`
+ Actions.labda{,.md}
+ `Properties.lagda{,.md}`
+ `Chain.lagda{,.md}`
+ `Ledger.Properties.Computational.lagda{,.md}`
+ `Ledger.Properties.lagda{,.md}`
+ `Test.StructuredContracts.lagda{,.md}`
+ `Ratify.lagda{,.md}`
+ `PParams.lagda{,.md}`
+ `Address.lagda{,.md}`
+ `Crypto.lagda{,.md}`
+ `TokenAlgebra.Base`
+ `TokenAlgebra.ValueSet`
+ PreConway files
@williamdemeo @carlostome
effect Carlos's change requests plus miscellaneous improvements
35eb5a0 
+ fix mkdocs hang issue
+ move EssentialAgda
+ switch to unicode character for em dash
+ fix broken links
+ revert removal of latex packages in flake (needed for diagram generation)
+ remove repeated console log
+ rename "Agda Essentials" -> "Essential Agda" to agree with module name
+ make reference-able NEWEPOCH section and add link to it
+ improve introduction and remove references to pdf generation
+ Update src/Interface/STS.lagda.md
+ Update src/Ledger/Conway/Specification/Gov/Actions.lagda.md
+ make paragraph less "out of the blue"
+ Update src/Ledger/Conway/Specification/Utxow.lagda.md

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
@williamdemeo
fix merge problem and include Dijkstra in toc
16cd457 
fix nix derivation and improve Epoch module

+ Remove dependency on formal-ledger from mkdocs
+ remove mkdocs-dev
+ revert some changes to flake.nix to make CI happy
+ Rename agdaWithPackages to fls-agdaWithPackages
+ Refactor formal-ledger dep. from html and hs-src
@williamdemeo
prepare to migrate many .agda files to .lagda.md
8a9282c 
...that we want to migrate.  There are still many `.agda` files in
`Conformance` and `Foreign` but we've decided they should not be
migrated and the corresponding html files should be removed from mkdocs
and not shown on the site.
@williamdemeo
complete migration of last set of .agda files
efa7448
@williamdemeo @carlostome
miscellaneous improvements
d20cdb9 
+ widen center region; make wide code blocks scroll
+ fix bug introduced by renaming
+ revert diffs introduced by bad conflict resolution
+ Reshuffle Gov.Actions
+ bugfix
+ Update src/Ledger/Conway/Specification/Gov/Actions.lagda.md

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
@williamdemeo
fix alignment, broken link, and missing import
ff1f3c9 
It seems fancy alignment in md is hard to get right (or doesn't work) when
vertical vectors are involved.
@williamdemeo williamdemeo force-pushed the 944-migrate-all-remaining-lagda-files branch from fdfc0d7 to 0a2ba7c Compare October 24, 2025 21:04
@williamdemeo williamdemeo merged commit a62d7e6 into master Oct 26, 2025
14 checks passed
@williamdemeo williamdemeo deleted the 944-migrate-all-remaining-lagda-files branch October 26, 2025 02:05
@williamdemeo williamdemeo self-assigned this Nov 11, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@carlostome carlostome carlostome approved these changes

Assignees

@williamdemeo williamdemeo

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Migrate all remaining .lagda files

2 participants

@williamdemeo @carlostome