(Picture taken in Δονούσα, Greece)

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

(Picture taken in Δονούσα, Greece)