Welcome to Galliblog, the Gallinette blog. I use the amazing omd markdown parser, and bits of parsing that I did myself. This is very much work in progress as of yet, but thanks to the power of omd you can already write pretty cool articles, simply.

This is a quote.

If you want to write markdown, this cheatsheet can be useful. Be careful that omd doesn't implement github flavoured markdown though. For instance, there is no strikethrough. But if there is a huge demand I can try to add it in.

You can highlight some code

Inline code like let x := 1 in x doesn't have any language affected to it, unless the default language is set in the header. (Note that it will set all inline codes and all block codes where the language is not specified.)

default language: coq

Lemma foo : forall n : nat, n = n.
Proof.
  intro n. reflexivity.
Qed.

let rec foo n =
  if n < 1 then 0 else foo (n - 1)

Syntax highlighting is done using highlight.js!

Typing some math

You can also write some math now! In this article I use KaTeX. MathJax is also available.

\[ \Delta \Vdash A \]

This should be inline \( f(x) = \alpha \).

This is inline too $\Xi \vdash t\sigma : A\sigma$ (however I do not recommend
using `$` as a delimiter for now because I don't handle it properly.)

$$\Gamma \vdash t : A$$

will display:

This should be inline \( f(x) = \alpha \).

This is inline too $\Xi \vdash t\sigma : A\sigma$ (however I do not recommend using $ as a delimiter for now because I don't handle it properly.)

Resources

Stuff you put in content/blog-resources will be made available in the resources directory. These are shared resources across the whole blog.

For instance the ugly coq logo.

Note: I might remove this later, don't know if this is really useful.

What's next

• Table of contents (since omd seem to provide it).
• Collect references to put at the end?
• Search (when it becomes necessary).
• Removing elm from the website.
• Render math on server.
• Highlight on server (add higlight choice).
• Write a proper tutorial.
• Not recompiling the whole blog if not necessary.
• Add mathjax as an alternative to KaTeX.
• Solve KaTeX problems backslash problem.