PLV@MIT

The PLV blog, built with Pelican and Alectryon. See the tutorial blogpost for details about Alectryon.

Local setup

Clone the plv/blog repository recursively (git clone --recurse-submodules) to get a copy of Alectryon (or use git submodule update --init to download it after cloning).

Dependencies:

opam install coq-serapi=8.10.0+0.7.0

python3 -m pip install --user pelican==4.2.0 markdown==3.1.1 docutils==0.16

python3 -m pip install --user pygments==2.5.2 dominate==2.4.0

Build:

make devserver (this will serve a live-updated copy of the blog at http://localhost:8000)

make rsync_deploy (this will upload the updated website to plv.csail.mit.edu)

Writing new posts

Write a draft, then make a PR to this repository.

Posts go to content/$year-$month-$day - $slug.$ext; you can use reStructuredText ($ext=rst) or markdown if you don't need advanced Coq highlighting ($ext=md). Pelican will generate one page per post, named $slug.html.

Here's a basic template for new posts (see the Pelican docs for more information), which you might put in e.g. content/2019-06-02 - short-title.rst:

============
 Post Title
============

:tags: t1, t2
:category: category-name
:authors: author1, author2
:summary: Short summary here.

.. preview::

   First few paragraphs, which will appear on the front page.

More text.

.. coq::

   Goal False -> True.
     intros.
     exact I.

You can render your new post using make devserver; the website will be at http://localhost:8000. If you want to share the rendered version, you can use make rsync_upload; the default configuration pushes to https://people.csail.mit.edu/$(SSH_USER)/plv-blog-drafts through login.csail.mit.edu.

Rendering your new post will create a .cache file along your .rst file. If your post requires a complex set-up, like external libraries, it's best to include the .cache file in your pull request.

Writing Coq proofs

Code in .. coq:: blocks is executed at build time; goals and responses are recorded and displayed along with the code.

Interacting with the proof

A small bubble next to a Coq fragment indicates that it produced output: readers can either hover, click, or tap on the fragment to show the corresponding goals and messages.

A special ‘Display all goals and responses’ checkbox is added at the beginning of the document; its position can be adjusted by adding an explicit .. alectryon-toggle:: directive.

Customizing the output

Directive arguments and special comments can be used to customize the display of Coq sessions. The documentation of Alectryon has details, but the easiest is probably to look at other blog posts for examples.

Tips

• Indent contents of .. coq:: directives three spaces deeper than the directive itself (further indentation is included in the output).

• To link to another blog post, such as /content/xyz.rst, use the following syntax:

  `A link to xyz <{filename}/xyz.rst>`_

• For reStructuredText tips, browse to https://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html.

• For help with Pelican, browse to https://docs.getpelican.com/en/stable/index.html.