Use highlightjs version 11 for Hakyll

So the other day I tried to add syntax highlighting for a new language to this blog.

Hakyll does support syntax highlighting and my previous setup also features a self-hosted pack of highlight.js. Previously they were somewhat working together, side by side. That is, whatever code I threw into the fenced block usually gets decently highlighted in the resulting webpage, so I didn’t care to know how.

However, when I searched my language in the big list, I realized that it wasn’t there. The way it works now is that highlightjs is provided as a library, on top of which third party languages can be added. Great, so I found out that mine was version 9 and I need to bump it to 11.

After the bump, I saw some warnings in the console. Turns out, between these two versions, a security patch is added to disable HTML passthrough and that’s where the warnings come from.

Wait a minute, I wasn’t writing any HTML in any of my code blocks. After some investigations, I found out that the HTML elements and attributes inside <code> were added by pandoc. They were meant to be used by the Hakyll syntax highlighting CSS. The solution? Disable those hints. The code blocks should be left as-is, to be handled by highlightjs.

So inside site.hs, instead of pandocCompiler, we want to use customPandocCompiler where

customPandocCompiler :: Compiler (Item String)
customPandocCompiler =
  pandocCompilerWith defaultHakyllReaderOptions writerOptions
  where
    writerOptions = defaultHakyllWriterOptions
      { writerHighlightStyle = Nothing }

That is, we changed the default style of Just pygment to Nothing, the same effect as the --no-highlight command line option.

With that, you should be able to replace highlight.pack.js with highlight.min.js and your-language.min.js.

If you still see type errors like 'name' is read-only, you might need to also bump the highlightjs version of your extension library.

As an example, I can now highlight Lean code with the highlightjs-lean extension and my bump. Behold the test file from the original repo:

import data.real.basic analysis.topology.topological_structures
open lattice set filter classical
noncomputable theory

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

@[simp]
lemma tauto : tt = tt := rfl

attribute [simp] zero_eq_zero

/-- Metric space
Each metric space induces a canonical `uniform_space` and hence a
canonical `topological_space`.  -/
class metric_space (α : Type u) extends uniform_space α : Type u :=
(dist : α → α → ℝ)
(dist_self : ∀ x : α, dist x x = 0)
(eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
(dist_comm : ∀ x y : α, dist x y = dist y x)
(dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
(uniformity_dist : uniformity = ⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε} . control_laws_tac)
(to_uniform_space := metric_space.uniform_space_of_dist dist dist_self dist_comm dist_triangle)


theorem tendsto_nhds_of_metric [metric_space β] {f : α → β} {a b} :
  tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0,
    ∃ δ > 0, ∀{x:α}, dist x a < δ → dist (f x) b < ε :=
⟨λ H ε ε0, mem_nhds_iff_metric.1 (H (ball_mem_nhds _ ε0)),
 λ H s hs,
  let ⟨ε, ε0, hε⟩ := mem_nhds_iff_metric.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
mem_nhds_iff_metric.2 ⟨δ, δ0, λ x h, hε (hδ h)⟩⟩ -- dash comment