emacs - 打开 emacs 时添加到 coqtop 的路径时，"Symbol' 作为变量的值是 void

Question

我正在尝试运行带有一般证明的 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 知道您正在编辑的文件类型，并且不会在编程模式下进行此类替换(除非您特意将其配置为这样做，在这种情况下，请不要这么做)。