Syntax highlighting is fun

I hope to talk about theorem proving from time to time. Since my tool of choice has been the Coq proof assistant, I thought I should find a way to display Coq code in these pages.

Jekyll allows to write using markdown syntax so I went looking for a way to get syntax highlighting. A post by Karl Urdevics suggests to use redcarpet and pygments, which is a syntax highlighter written in Python.

Turns out pygments does support Coq. Here is how it looks:

Lemma andb_true_inversion:
  forall b1 b2 : bool,
    andb b1 b2 = true <-> b1 = true /\ b2 = true.
Proof.
  split.
  - case_eq b1; case_eq b2; auto.
  - apply andb_true_intro.
Qed.

The list of supported languages is quite impressive and includes some of my favorites. Here is an example in OCaml:

let rec fib x =
  if x <= 1
  then 1
  else fib (x - 1) + fib (x - 2);;

Here is an example in SQL:

SELECT count(*)
FROM employees
WHERE age > 32;

And it even supports XQuery, which is a language I worked on for many years:

<result>{
  for $x in ("Hello"," ","world!") return $x
}</result>

Pretty cool! How to setup Jekyll for both wasn’t entirely clear at first, mostly because I am not very familiar with Jekyll and Ruby. What worked for me was first to install the right gems (i.e., Ruby packages). Turns out the name for the pygments one is pygments.rb:

$ gem install redcarpet
$ gem install pygments.rb

Then to add those two packages to the Gemfile in my Jekyll project as follows:

...
# This will help ensure the proper Jekyll version is running.
# Happy Jekylling!
gem "jekyll", "~> 3.6.2"
gem 'redcarpet', '~> 3.4.0'    # Added
gem 'pygments.rb', '~> 1.2.0'  # Added
...

Without forgetting to run bundle install since, I have been using Bundler as well (I cannot quite recall why).

Finally, I had to update the _config file for my Jekyll project:

# Conversion
markdown: redcarpet
highlighter: pygments