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:

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:

-- 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 using Hakyll snapshots, you should take a snapshot before running Alectryon.tryTransform_.

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:

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