Hakyll plugin for Alectryon [![Hackage](https://img.shields.io/hackage/v/hakyll-alectryon.svg)](https://hackage.haskell.org/package/hakyll-alectryon)
===========================

[Alectryon][alectryon] is a tool for pretty-printing Coq proofs,
notably rendering proof states between tactics.

This package, *hakyll-alectryon*, integrates Alectryon with the Hakyll site
generator.

[alectryon]: https://github.com/cpitclaudel/alectryon
[pygments]: https://pygments.org

## Dependencies

To use this package, first install [Alectryon][alectryon].
The executables `alectryon` and `python3` must be on your `$PATH`.

(Pygments is also used by this package, and is required by Alectryon anyway.)

## Usage

The simplest way to use this package is to stick the `tryTransform_` function
in a compiler for Markdown blog posts:

```haskell
-- Main.hs
import qualified Hakyll.Alectryon as Alectryon

main :: IO ()
main = hakyll $ do
  (...)
  match "blog/*.md" $ do
    (...)
    compile $ do
      (...)
      Alectryon.tryTransform_ doc >>= (...)
```

This will process all `alectryon` and `coq` code blocks using Alectryon and
Pygments, respectively.

- `alectryon` code blocks are the actual parts of the literate program which
  will be interpreted. Interactive proof states will be rendered.
- `coq` code blocks are just for show. They will only go through syntax
  highlighting using Pygments, in roughly the same style as Alectryon.

Options can be passed to Alectryon to find Coq dependencies,
via the metadata header of each post:

```
---
title: My awesome post
alectryon: ["-Q", "my/coq/lib", "MyCoqLib"]
---
```

The compiled `.vo` files must already be present.

### Modular usage

You can also allow your blog to be built without requiring those
external dependencies, by caching the output of Alectryon and Pygments
and checking it into version control (git).

Create a cache directory for each document that uses hakyll-alectryon,
and write its path in the `alectryon-cache` field of the document.
The `alectryon` field must also be set; use the empty list by default.

```
---
title: My awesome post
alectryon: []
alectryon-cache: "blog/my-awesome-post/cache"
---
```

The Hakyll site generator must also be modified to add a command-line option to
generate the cache or to use the cache. Replace `Hakyll.hakyll` with
`Alectryon.hakyll`, and pass the option to `Alectryon.tryTransform`:

```haskell
-- Main.hs
import qualified Hakyll.Alectryon as Alectryon

main :: IO ()
main = Alectryon.hakyll $ \opts -> do
  (...)
  match "blog/*.md" $ do
    (...)
    compile $ do
      (...)
      Alectryon.tryTransform opts doc >>= (...)
```

When writing a post, build your site with the option `--run-alectryon` to interpret
your literate Coq file with Alectryon.

```
# Whenever 'coq' and 'alectryon' code blocks change or are reordered
cabal exec mysite -- build --run-alectryon
```

When the post is finished, add the cached outputs to version control.
These are two files `alectryon.html` and `pygments.html`.

```
# If the cache is set to "alectryon-cache: "blog/my-awesome-post/cache"
git add blog/my-awesome-post/cache/*.html
git commit
```

As long as you don't modify the code blocks, the site can be compiled normally,
without any dependency on Alectryon, Coq, or Python.

```
# As long as the 'coq' and 'alectryon' code blocks haven't changed
cabal exec mysite -- build
```

If the code blocks are modified, you must enable `--run-alectryon` again to
reprocess them and update the cache.

See also the [`example/`](./example) directory for a minimal example.