Hello Verso

February 14, 2026

berberman

Meta

2 min read

It's been 6 years since I first built this site using Hakyll—though I barely posted anything. Recently, I decided to migrate to Verso, a new static site generator written in Lean. It allows me to write posts directly in Lean and seamlessly integrating code snippets:

import VersoBlog
import Blog.Categories
import Blog.Site.Extensions
open Verso Genre Blog

#doc (Post) "Hello Verso" =>

%%%
authors := ["berberman"]
date := {year := 2026, month := 2, day := 14}
categories := [Category.meta]
%%%

```leanInit empty
```

It's been 6 years since I first built this site using [Hakyll](https://github.com/jaspervdj/hakyll)—though I barely posted anything.
Recently, I decided to migrate to [Verso](https://github.com/leanprover/verso),
a new static site generator written in Lean. It allows me to write posts directly in Lean and seamlessly integrating code snippets:

```lean empty
theorem Eq.uip {α : Sort u}
    (x y : α) (h₁ h₂ : x = y) : h₁ = h₂ := byα:Sort ux:αy:αh₁:x = yh₂:x = y⊢ h₁ = h₂
  rflAll goals completed! 🐙

Nat.succ (n : Nat) : Nat#check Nat.succ

Nat.succ (n : Nat) : Nat

I adapted this site from verso-templates, and with some fine-tuning, I've got Prism.js working for non-Lean languages:

main :: IO ()
main = putStrLn "Hello, World!"

and typst with mathyml for typesetting math $𝑓 (𝑥)$ formulas:

$(\frac{1}{\sqrt{2 𝜋}}) 𝑒^{- \frac{𝑥^{2}}{2}} (\begin{matrix} 1 & 2 \\ 3 & 4 \end{matrix})$

$𝜋 (𝑥)$

$\frac{𝑎}{𝑏}] = 𝑎 = {\frac{𝑎}{𝑏})$

$(\begin{matrix} 1 & 0 & 1 \\ 0 & 1 & 2 \end{matrix})$

$(\begin{matrix} 11 & 12 & 13 & 14 & 15 \\ 21 & 22 & 23 & 24 & 25 \\ 31 & 32 & 33 & 34 & 35 \\ 41 & 42 & 43 & 44 & 45 \end{matrix})$

I hope to use this refresh to share more updates and thoughts on programming. Stay tuned!