Hakyll plugin for 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.

Dependencies

To use this package, first install 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:

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

-- 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/ directory for a minimal example.