Skip to content

Conversation

@williamdemeo
Copy link
Member

Description

This PR begins the migration of LaTeX-based literate Agda source code (.lagda files) to Markdown-based literate Agda (.lagda.md files).

Migration Process

  1. Enter the markdown nix shell by running nix develop .#markdown in the main repo directory.
  2. Place a copy of the .lagda file to be migrated to the appropriate directory under src_legacy; example: place a copy of src/Ledger/Introduction.lagda in src_legacy/Ledger/Introduction.lagda.
  3. Rename the file to be migrated using git mv and change the extension from .lagda to .lagda.md; example: git mv src/Ledger/Introduction.lagda{,.md}.
  4. Commit the name change before replacing the contents of the file with Markdown. This helps ensure the git history of the file is preserved.
  5. Edit the Markdown file produced by the build script in _build/mkdocs/src and launch the web site server to check that it looks okay; example: edit the file _build/mkdocs/src/docs/Ledger.Introduction.md, change to the _build/mkdocs/src directory and run mkdocs serve.
  6. Copy the changes to the literate Markdown made in step 4 to the corresponding .lagda.md file under _build/mkdocs/agda_snapshot_src.
  7. Replace the LaTeX content with Markdown; example: copy the contents of _build/mkdocs/agda_snapshot_src/Ledger/Introduction.lagda.md into src/Ledger/Introduction.lagda.md, removing the LaTeX content that was there before.

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 May 23, 2025 that may be closed by this pull request
@williamdemeo
Copy link
Member Author

Closing this PR because 1. migration approach will change so file history is actually preserved and 2. this branch shouldn't be part of a PR (to be merged to master) just yet, but rather should be kept as a separate branch for now.

@williamdemeo williamdemeo deleted the 788-markdown-migration-phase1 branch October 2, 2025 03:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

begin migration to markdown

2 participants