0.0
The project is in a healthy, maintained state
This Jekyll plugin allows to you write literate Agda. It will compile your code using Agda itself, producing beautifully highlighted and hyperlinked pages.
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
 Dependencies

Development

~> 11.1.3
~> 3.10.0
~> 0.13.0
~> 0.21.2

Runtime

>= 3, < 5
 Project Readme

jekyll-agda

CI tests status badge Latest release badge License badge Maintainability badge Test coverage badge

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.

  1. 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
  2. Add Agda interface files to Jekyll's list of exclusions in _config.yml:

    # _config.yml
    exclude:
      - "*.agdai"
  3. Add Agda interface files and jekyll-agda's work dir to your .gitignore:

    # .gitignore
    *.agdai
    .agda-html/
  4. 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