jekyll-agda is a Jekyll plugin which allows you to use literate Agda for your website and take full advantage of its highlighting and hyperlinking features.
Assuming you have a working Agda installation and a Jekyll website already set up, you need to do just four things.
-
Add the
jekyll-agdagem to your plugins in theGemfileand runbundleto install it:# Gemfile group :jekyll_plugins do gem "jekyll-agda" end
-
Add Agda interface files to Jekyll's list of exclusions in
_config.yml:# _config.yml exclude: - "*.agdai"
-
Add Agda interface files and
jekyll-agda's work dir to your.gitignore:# .gitignore *.agdai .agda-html/ -
Add Agda's default stylesheet (which
jekyll-agdawill produce) to the<head>of your layout:<link rel="stylesheet" href="{{ '/lagda/Agda.css' | relative_url }}" />
That's it! You can now write your posts and pages using literate Agda.
Here is a sample post you can save as _posts/2022-01-14-foobar.lagda.md to get started:
---
title: My first literate Agda post
---
Let's define Peano's natural numbers:
```agda
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
```
Is `Set` clickable? Yes it is.
And the other keywords too!
Right now this plugin is an MVP and accepts no configuration, so Getting started covers pretty much everything about its usage.
The only caveat is: write your code in unnamed independent modules to be totally safe. Otherwise, Agda and Jekyll naming conventions might be at odds. You can definitely try do more complex stuff though! I simply haven't given this enough thought yet to clearly spell out the details (see last point of the Roadmap).
Here is a roadmap of features I think would be useful.
- Custom output path/url instead of hardcoded
/lagda - Custom stylesheet instead of Agda's default
Agda.css - Custom layout for
/lagda/*pages (leveraging--html-highlight=codeinstead of--html-highlight=auto) - Find some convenient way to knit Agda and Jekyll naming conventions:
- Currently all pages are compiled as independent "root" files, so Agda is not affected by Jekyll's conventions as long as you don't define a
modulein your files - Structuring code in multiple files/modules is doable but will require some clever dependency management to avoid redundant compilations
- Ideally, we'd like complete freedom in structuring code to do stuff like multiple pages corresponding to modules, or a series of posts in which later ones import the previous ones
- Currently all pages are compiled as independent "root" files, so Agda is not affected by Jekyll's conventions as long as you don't define a
- Find a way to support highlighting and hyperlinking for inline code, i.e. for markdown fragments like
`Set`{:.agda}.
Of course any feedback is welcome!
- Thanks to @conal for prompting me with the idea.
