使 Hexo 支持高亮 Lean

说真的，Hexo 这么烂下去我真要换 Hugo 了——为什么它甚至不支持给 hljs 添加语言插件？

好吧，这篇博客讲述如何让你的 Hexo 博客支持高亮 Lean，并且是后端渲染。

Step 1. 安装 highlightjs-lean ¶

问题的起因就是 hljs 并不默认支持 lean，因此必须手动安装之。在你的 hexo 博客根目录进行：

npm install highlightjs-lean
# 或者 yarn add highlightjs-lean

Step 2. 将 Lean 语言支持添加到 hljs ¶

你需要创建一个简单的 hexo 插件做这件事情。在你的 hexo 博客根目录新建 scripts 文件夹，随意新建一个 javascript 文件，名字自取，例如 add-lean.js

在该 js 文件中写入以下内容：

const hljs = require('highlight.js');
const leanHljs = require('highlightjs-lean');
hljs.registerLanguage("lean", leanHljs);

这样就注册了 lean 的语言支持

Step 3. 把 hexo-utils 的语言定义文件里添加上 Lean ¶

如果你做了上述操作，恭喜你，至少 autodetect 能尝试识别 Lean 了。但是 hljs 的 autodetect 众所周知的不准确，于是你尝试在代码块中指定语言为 lean，嘿，hexo 反而自动给你转成 plaintext了~

在这三行中揭示了原因。 hexo-utils 使用了一个 hard-coded 的 highlight_alias.json 文件，任何不在这个 json 文件中的语言都会直接被视作 plaintext， 我不懂它为什么要这样干，hljs 明明提供了 api 让你获得 available 的语言，但它就是这么干了。

const alias = require('../highlight_alias.json');

function highlight(str: string, options: Options) {
  //...
  if (!lang || !alias.aliases[lang]) {
    lang = 'plaintext';
  }

由于这个文件是硬编码的，你甚至不能更改它。所以插件在这里有些苍白无力。你不得不写一个 不是插件的脚本（比如 pre-deploy.js），在每次deploy前把该文件修改一下：

const fs = require("fs");

const alias = JSON.parse(fs.readFileSync("node_modules/hexo-util/highlight_alias.json").toString());

alias.aliases["lean"] = "lean";
alias.languages.push("lean");

fs.writeFileSync("node_modules/hexo-util/highlight_alias.json", JSON.stringify(alias));

然后在你每次 deploy 前，需要执行一下

node pre-deploy.js

把该文件修改后，hexo 终于支持了 lean 语言的高亮。

成果展示 ¶

import MIL.Common

open Nat

-- These are pieces of data.
#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

-- These are propositions, of type `Prop`.
#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

-- These are proofs of propositions.
theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

-- Here are some proofs.
example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say m and n are natural numbers, and assume n=2*k.
  rintro m n ⟨k, hk⟩
  -- We need to prove m*n is twice a natural number. Let's show it's twice m*k.
  use m * k
  -- Substitute for n,
  rw [hk]
  -- and now it's obvious.
  ring

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]