Meta
-
Hello Verso
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₂ := α:Sort ux:αy:αh₁:x = yh₂:x = y⊢ h₁ = h₂ All goals completed! 🐙#check Nat.succI adapted this site from verso-templates, and with some fine-tuning, I've got Prism.js working for non-Lean languages:
Read moremain :: IO () main = putStrLn "Hello, World!" -
More Verso
This blog has been around for a while, but every time I visited it, something about the visual design felt off. The typography was not elegant enough; Lean code blocks had no color scheme; the palette lacked quality; and the font size were not quite right. Overall, the site did not feel modern, and both UI and UX needed work, even though it retained kind of minimalist style. RSS/Atom feeds were also missing.
So I decided to refine the styling on top of existing foundation, and add a few interesting features.
Read more