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]:

```
pip install alectryon
opam install coq-serapi  # OCaml package used by alectryon
```

The executables `alectryon` and `python3` must be on your `$PATH`.
(`python3` is used to load Pygments, which is required by Alectryon anyway.)

## Basic 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 that your post depends on must already be present
(Alectryon will not compile dependencies for you).

You should also add the CSS file from the Alectryon repository (MIT Licensed)
to your blog: `alectryon/assets/alectryon.css`.

### Caution advised for RSS and Atom feeds

If your blog has an RSS or Atom feed, readers might not get the CSS files to
render proof scripts properly.
If your feed follows [the Hakyll tutorial](https://jaspervdj.be/hakyll/tutorials/05-snapshots-feeds.html)
using Hakyll snapshots, you should take a snapshot before running
`Alectryon.tryTransform_`.

```haskell
compile $ do
  (...)
  _ <- saveSnapshot snap (writePandoc doc)
  Alectryon.tryTransform_ doc >>= (...)

{- INSTEAD OF
  Alectryon.tryTransform_ doc >>= (...) >>= saveSnapshot snap >>= (...)
-}
```

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