在 coq-mode 下开启行号显示

行号（Line Number）的显示，似乎不应该成为一个问题。vscode 仓库里还有一个 issue 在询问怎么方便地关闭行号显示。而对于 Vim 用户来说，一句 set :number 就可以开启行号显示。

没错，Emacs 就是这么特别的编辑器。对我这样偶尔用一用的用户来说，行号显示也确实是一个困扰我的问题。

❖问题是什么

我使用的是一个 Emacs 的发行版，或者说一个比较成熟的配置文件，Spacemacs. 在 Spacemacs 的官方文档里，要开启行号显示，似乎只需要在 .spacemacs 里设置一下变量就可以了：

1(setq-default dotspacemacs-line-numbers t)

这句话的意思就是，把 dotspacemacs-line-numbers 设置为 t.

同时，为了支持 coq 语言，我还装载了 coq 层（layer）. 但如果打开一个 coq 文件，你也许会惊奇地发现，这时 coq 源代码是没有行号的：

按照正常的直觉，设置为 t 应该是会在所有情况下显示行号的。那么，为什么没有显示行号呢？

❖临时解决方案

解决这个问题，其实比搞清楚原因要容易。

稍加搜索，我发现 spc t n 1可以在当前 buffer 打开行号，这确实可以解决问题。按照 Emacs wiki 的说法，这个快捷键调用的实际上是 Emacs 26.1 版本后引入的行号命令 display-line-numbers-mode.

Emacs 的命令可以通过 m-x，或者 spc spc 执行。实际上，一个命令就是一个 Emacs Lisp 的函数，参考 Programming Elisp 的文档，只要一个函数的函数定义里有 (interactive)，那么它就可以当成一个命令调用。

显然，Spacemacs 也是通过这个函数进行行号相关设置。虽然不知道因为什么原因，Spacemacs 没有给我的 .v 文件开启行号，但是我们可以自己开启。

coq 层实际上使用了 coq-mode. coq-mode 是一个 Emacs 的主模式（Major Mode），它给 coq 语言提供了支持，并定义了一大堆快捷键。

Emacs 支持一种叫做 Hooks 的机制，它允许我们在某个模式加载时，执行一系列操作。既然 Spacemacs 不会给 coq-mode 开启行号，我们就通过这种机制手动执行 display-line-numbers-mode.

1(defun dotspacemacs/user-config ()
2  "Configuration for user code:
3This function is called at the very end of Spacemacs startup, after layer
4configuration.
5Put your configuration code here, except for variables that should be set
6before packages are loaded."
7  (add-hook 'coq-mode-hook (lambda () (display-line-numbers-mode 1)))
8)

这里的 dotspacemacs/user-config 是 Spacemacs 配置文件的一部分，在这里可以执行一些自定义操作。

这当然就解决了问题。其实，Spacemacs 在文档里还提到了一个选项 :enabled-for-modes. 在这个选项里加上 coq-mode 可以直接解决问题。不过我直到搞清楚了问题的来源，才发现了有这个选项。

1(setq-default dotspacemacs-line-numbers
2  '(:enabled-for-modes coq-mode))

❖为什么

我首先注意到的是 dotspacemacs-line-numbers 的注释：

1;; Control line numbers activation.
2;; If set to `t', `relative' or `visual' then line numbers are enabled in all
3;; `prog-mode' and `text-mode' derivatives. If set to `relative', line
4;; numbers are relative. If set to `visual', line numbers are also relative,
5;; but only visual lines are counted. For example, folded lines will not be
6;; counted and wrapped lines are counted as multiple lines.
7;; This variable can also be set to a property list for finer control:
8;; (default nil)

这段注释里提到，如果把这个变量设置为 t，那么它会默认在 prog-mode 和 text-mode 里开启行号。这两个 mode 被称为 Basic Major Mode. 一个很自然的猜想是, coq-mode 不是它们之一。

打开一个 coq 文件，执行 m-x describe-mode，会看到：

1Coq mode defined in ‘coq-mode.el’:
2Major mode for Coq scripts.

进入 coq-mode.el 的源代码查看一下，玄机就在第 182 行：

1(defun coq--parent-mode ()
2  (if coq-use-pg (proof-mode) (prog-mode)))
3
4;;;###autoload
5(define-derived-mode coq-mode coq--parent-mode "Coq"
6  "Major mode for Coq scripts.

这个 coq--parent-mode 显然就是 coq-mode 的父模式（parent mode），Emasc 的模式也有一个继承树，一个模式继承另一个父模式，这棵树的根不确定，有几种情况：

  • 自己
  • Fundamental Mode
  • Basic Major Mode

coq-use-pg 的值在我的环境里为 t，它的父模式是 proof-mode. proof-mode 的父模式又是什么呢？

StackOverflow 的一个问题提供了相关代码：

1(defun derived-modes (mode)
2  "Return a list of the ancestor modes that MODE is derived from."
3  (let ((modes   ())
4        (parent  nil))
5    (while (setq parent (get mode 'derived-mode-parent))
6      (push parent modes)
7      (setq mode parent))
8    (setq modes  (nreverse modes))))

用这个函数，确实可以得到一些“正常”模式的继承路径，比如我们刚刚说的 proof-mode:

1ELISP> (derived-modes 'proof-mode)
2(prog-mode)

是的，proof-mode 的父模式就是 prog-mode. 如果你还记得刚才的文档的话，prog-mode 在 dotspacemacs-line-numbers 设置为 t 的时候也应该显示行号。

那么，究竟是什么地方错了呢？不妨给这个函数输入 'coq-mode:

1ELISP> (derived-modes 'coq-mode)
2(coq--parent-mode)

它的输出是 (coq--parent-mode)，这只是父模式的符号，而不是求值后的父模式。可见，(get 'coq-mode 'derived-parent-mode) 这个表达式只能拿到语法上的符号，而非它真正的父模式。检查 define-derived-mode 的源代码，可以发现 (get mode 'derived-mode-parent) 拿到的是这句话设置的父模式：

1(put ',child 'derived-mode-parent ',parent)

那么，Spacemacs 是这样得到父模式的吗？Spacemacs 在 spacemacs/layers/+spacemacs/spacemacs-defaults/funcs.el 的 spacemacs//linum-enabled-for-current-major-mode 函数中检查是否在当前模式下开启行号显示：

1(defun spacemacs//linum-enabled-for-current-major-mode ()
2  "Return non-nil if line number is enabled for current major-mode."
3  (let* ((disabled-for-modes
4          (spacemacs/mplist-get-values dotspacemacs-line-numbers
5                                       :disabled-for-modes))
6         (user-enabled-for-modes
7          (spacemacs/mplist-get-values dotspacemacs-line-numbers
8                                       :enabled-for-modes))
9         ;; default `enabled-for-modes' to '(prog-mode text-mode), because it is
10         ;; a more sensible default than enabling in all buffers - including
11         ;; Magit buffers, terminal buffers, etc. But don't include prog-mode or
12         ;; text-mode if they're explicitly disabled by user
13         (enabled-for-modes (or user-enabled-for-modes
14                                (seq-difference '(prog-mode text-mode)
15                                                disabled-for-modes
16                                                #'eq)))
17         (enabled-for-parent (or (and (equal enabled-for-modes '(all)) 'all)
18                                 (apply #'derived-mode-p enabled-for-modes)))
19         (disabled-for-parent (apply #'derived-mode-p disabled-for-modes)))
20    (or
21     ;; special case 'all: enable for any mode that isn't specifically disabled
22     (and (eq enabled-for-parent 'all) (not disabled-for-parent))
23     ;; current mode or a parent is in :enabled-for-modes, and there isn't a
24     ;; more specific parent (or the mode itself) in :disabled-for-modes
25     (and enabled-for-parent
26          (or (not disabled-for-parent)
27              ;; handles the case where current major-mode has a parent both in
28              ;; :enabled-for-modes and in :disabled-for-modes. Return non-nil
29              ;; if enabled-for-parent is the more specific parent (IOW derives
30              ;; from disabled-for-parent)
31              (spacemacs/derived-mode-p enabled-for-parent disabled-for-parent)))
32     ;; current mode (or parent) not explicitly disabled
33     (and (null user-enabled-for-modes)
34          enabled-for-parent            ; mode is one of default allowed modes
35          disabled-for-modes
36          (not disabled-for-parent)))))

可以看到，它通过 derived-mode-p 函数询问当前 buffer 的 major mode 是不是预设的 enabled-for-modes 的子模式。dervied-mode-p 是 Emacs 提供的一个函数，文档声称，如果当前 buffer 的主模式是 modes 的子模式，那么 (derived-mode-p modes) 将返回非 nil 值。

再检查 derived-mode-p 的源代码，我们终于发现了问题的根源。

1(defun provided-mode-derived-p (mode &rest modes)
2  "Non-nil if MODE is derived from one of MODES or their aliases.
3Uses the `derived-mode-parent' property of the symbol to trace backwards.
4If you just want to check `major-mode', use `derived-mode-p'."
5  (while
6      (and
7       (not (memq mode modes))
8       (let* ((parent (get mode 'derived-mode-parent))
9              (parentfn (symbol-function parent)))
10         (setq mode (if (and parentfn (symbolp parentfn)) parentfn parent)))))
11  mode)
12
13(defun derived-mode-p (&rest modes)
14  "Non-nil if the current major mode is derived from one of MODES.
15Uses the `derived-mode-parent' property of the symbol to trace backwards."
16  (apply #'provided-mode-derived-p major-mode modes))

dervied-mode-p 同样通过 (get mode 'derived-mode-parent) 来得到某个模式的父模式，而这对于 coq-mode 来说会得到 coq--parent-mode, 继承链在这里就断了。

Emacs 中的模式定义最后确实是定义了一个函数。然而，如果 'parent 不能求值出正确的父模式，Emacs 对于 mode 的预设函数就会得不到期望的结果。显然，coq-mode 不应该这样定义 coq--parent-mode. 那么，到底应该怎么定义 coq--parent-mode 呢？

❖最终解决方案

Emacs Lisp 的全局变量和全局函数是不同的，这和 Scheme 很不一样。如果直接把 coq--parent-mode 定义为一个变量，会使得 coq-mode 无法加载。

1(defvar coq--parent-mode
2  (if coq-use-pg 'proof-mode 'prog-mode))

万幸的是，Emacs Lisp 提供了一个叫做 defalias 的函数，它可以把 coq--parent-mode 定义为一个 alias.

1(defalias 'coq--parent-mode
2  (if coq-use-pg 'proof-mode 'prog-mode))

上面的修改就足以使得 Spacemacs 可以自动侦测到 coq-mode 派生自 prog-mode，从而开启行号显示。我已经提交了一个 PR，并合入了主分支。