IntersectMBO / IntersectMBO/formal-ledger-specifications

Literate Agda using markdown

Open
#680 16 comments 0 reactions 0 assignees View on GitHub
discussion documentation
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.

![Image](https://github.com/user-attachments/assets/43a9dd87-310a-4eba-82a2-39156560745d)

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

![Image](https://github.com/user-attachments/assets/0e8185d8-7cda-4ed6-bfc4-5ade568009be)

Versus this section from this repo:

https://github.com/IntersectMBO/formal-ledger-specifications/blob/master/src/Ledger/GovernanceActions.lagda

Screenshot formal-ledger-specifications

![Image](https://github.com/user-attachments/assets/9b69d63a-2596-4d66-9a52-d0ab480c469f)

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.