jekyll-agda

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.

Getting started

Assuming you have a working Agda installation and a Jekyll website already set up, you need to do just four things.

Add the jekyll-agda gem to your plugins in the Gemfile and run bundle to 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-agda will 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!

Usage

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).

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=code instead 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 module in 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
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!

Acknowledgements

Thanks to @conal for prompting me with the idea.

jekyll-agda

Development

Runtime

jekyll-agda

Getting started

Usage

Roadmap

Acknowledgements