IntersectMBO / IntersectMBO/formal-ledger-specifications
Literate Agda using markdown
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
Opening this issue as I would like to discuss whether there is a chance to create the formal-ledger-specifications as a set of literate Agda documents _using markdown instead of LaTeX_.
## Why
As an occasional reader of the `formal-ledger-specfications` I want to be able to contribute to it by fixing typos, fixing links or even suggesting "prose" and explanations to make certain dense concepts more easier to understand to readers. i.e. this request is not about the Agda code itself.
While I know how to write LaTeX, I prefer using less distracting formats like markdown or restructured text. As I post this issue here in Github, I am typing it in (github flavored) markdown and hence this feels most familiar to me as a software engineer.
Furthermore, as a "casual contributor" I might be even reading the specification and when finding a small issue like a typo, I would not have the repo checked out, but prefer to "edit in github" (there are links like this often in rendered documents to invite collaborators).
## What
Should we use [Literate Markdown](https://agda.readthedocs.io/en/v2.7.0/tools/literate-programming.html#literate-markdown-and-typst) to write the Ledger specs?
## Example
I really like how the [Programming Language Foundations in Agda](https://plfa.github.io/) book is presented and when I briefly worked on it in a workshop it was very easy to contribute to as it is just Markdown + Agda code blocks. The pull request even rendered a nice "rich" diff: https://github.com/plfa/plfa.github.io/pull/878/files#diff-2a2528d7e68ace2c2a17503f240dc0933d52fadf03cdab452b34a513bf6ebfca.

With literate markdown, Github helps me to access and re-orient myself in the corresponding source file. Compare this section from [plfa](https://github.com/plfa/plfa.github.io):
https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part1/Induction.lagda.md
Screenshot plfa

Versus this section from this repo:
https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/GovernanceActions.lagda
Screenshot formal-ledger-specifications

Contributor guide
Assessment
This issue has not been assessed yet.