この記事はChatGPTによって中国語から翻訳されたもので、いくつかの誤りが含まれているかもしれません。不正確な部分があればご了承ください。
行番号（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レイヤーをロードしました。しかし、coqファイルを開くと、驚くことに、この時点ではcoqのソースコードには行番号が表示されません：
通常の直感では、tに設定するとすべての状況で行番号が表示されるはずです。では、なぜ行番号が表示されないのでしょうか？
§一時的な解決策
この問題を解決するのは、原因を理解するよりも簡単です。
少し検索してみると、spc t n 1で現在のバッファに行番号を表示できることがわかりました。これは確かに問題を解決します。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 の行番号が有効になると述べています。これらのモードは 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）で、Emacsのモードにも継承ツリーがあり、一つのモードが他の親モードを継承します。このツリーのルートは確定していませんが、いくつかのケースがあります：
- 自分自身
- 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 関数を使って現在のバッファの major mode が予設の enabled-for-modes の子モードであるかどうかを問い合わせています。dervied-mode-p はEmacsが提供する関数で、ドキュメントによれば、現在のバッファの主モードが 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のモードに対する予設関数は期待した結果を得られません。明らかに、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 をエイリアスとして定義することができます。
1(defalias 'coq--parent-mode
2 (if coq-use-pg 'proof-mode 'prog-mode))上記の修正だけで、Spacemacsは coq-mode が prog-mode から派生していることを自動的に検出し、行番号の表示を開始できます。私はすでに PR を提出し、主分支にマージしました。