hakyll-alectryon: Hakyll extension for rendering Coq code using Alectryon

[ library, mit, text, web ] [ Propose Tags ]

An extension to write Literate Coq blog posts using Hakyll.

hakyll-alectryon extends the Hakyll site generator with the Alectryon documentation tool for Coq.

See also the README.


[Skip to Readme]
Versions [faq] 0.1.0.0, 0.1.1.0
Change log CHANGELOG.md
Dependencies aeson, base (>=4.9 && <5), bytestring, filepath, hakyll (>=4), mtl, optparse-applicative, pandoc, pandoc-types, process, text [details]
License MIT
Copyright Li-yao Xia 2020
Author Li-yao Xia
Maintainer lysxia@gmail.com
Category Text, Web
Home page https://gitlab.com/lysxia/hakyll-alectryon
Bug tracker https://gitlab.com/lysxia/hakyll-alectryon/-/issues
Source repo head: git clone https://gitlab.com/lysxia/hakyll-alectryon
Uploaded by lyxia at 2020-10-08T19:25:26Z
Distributions NixOS:0.1.1.0
Downloads 71 total (7 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2020-10-08 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for hakyll-alectryon-0.1.1.0

[back to package description]

Hakyll plugin for Alectryon Hackage

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.