在打开emacs时添加路径到coqtop时，“Symbol的值作为变量是空的”

Question

我正在尝试使用proof generale运行emacs来打开Coq文件。但是，当我打开emacs时，我得到以下错误消息：

Symbol's value as variable is void: “/Users/myusername/.opam/default/bin/coqtop”

我的emacs文件如下：

(setq coq-prog-name “/Users/username/.opam/default/bin/coqtop”)

(require 'package) ;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) (package-initialize)

(custom-set-variables  ;; custom-set-variables was added by Custom.  ;; If you edit it by hand, you could mess it up, so be careful.  ;; Your init file should contain only one such instance.  ;; If there is more than one, they won't work right.  '(package-selected-packages '(proof-general))) (custom-set-faces  ;; custom-set-faces was added by Custom.  ;; If you edit it by hand, you could mess it up, so be careful.  ;; Your init file should contain only one such instance.  ;; If there is more than one, they won't work right.  )

关于如何让我的emacs与coqtop一起工作有什么建议吗？

Answer 1

Emacs将“/Users/myusername/.opam/default/bin/coqtop”视为一个符号，因为它是一个普通字符序列。它不是以(ASCII)双引号开头，而是以字符“开头，以字符”结尾。它们不是ASCII左右双引号。使用ASCII引号"，这是Emacs Lisp (和许多其他编程语言)中的字符串分隔符。

(setq coq-prog-name "/Users/username/.opam/default/bin/coqtop")

不要使用文字处理程序编辑源代码，因为文字处理程序会插入“智能引号”和其他供人类阅读的功能。编辑Emacs配置的最佳位置是Emacs本身。Emacs知道您正在编辑什么类型的文件，并且不会在编程模式下进行这样的替换(除非您已经特意将其配置为这样做，在这种情况下，请不要这样做)。