Skip to content
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.

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

[ literate ] Support typst in literate Idris #3403

Merged
merged 2 commits into from
Nov 7, 2024

Conversation

buzden
Copy link
Contributor

@buzden buzden commented Oct 26, 2024

Description

Typst is relatively young typesetting system which aims to be as powerful as TeX while being lightweight more like Markdown and extensible by programmers with custom libraries (and tens of them are already around).

I personally use Pandoc Markdown + raw TeX insertions with Literate Idris for my papers and presentations, and I find this facinating, especially an ability to compile and run my slides and thus to check all the code on them during build of a PDF. I'd like to use typst too for that, but now compiler does not support it, which is not much a change.

So, I suggest to add the support for typst files. Also I made a small refactoring in a separate commit, and I tried to correct/extend existing literate Idris documentation.

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md (and potentially also
    CONTRIBUTORS.md).

@buzden buzden force-pushed the typst-literate-idris branch 2 times, most recently from a66b00d to 947d014 Compare October 27, 2024 04:23
@andrevidela
Copy link
Collaborator

@gallais are we waiting on something to merge?

@gallais
Copy link
Member

gallais commented Nov 6, 2024

Would be nice to have a test

@buzden
Copy link
Contributor Author

buzden commented Nov 6, 2024

I've added a test to the last commit

@gallais gallais merged commit 65ff121 into idris-lang:main Nov 7, 2024
22 checks passed
@buzden buzden deleted the typst-literate-idris branch November 7, 2024 14:40
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.

4 participants