"Symbol's value as variable is void" 在打开 emacs 时添加到 coqtop 的路径
"Symbol's value as variable is void" when adding a path to coqtop when opening emacs
我正在尝试 运行 emacs with proof generale 打开 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 一起工作有什么建议吗？
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 知道您正在编辑什么类型的文件，并且不会在编程模式下进行此类替换（除非您特意将其配置为这样做，在这种情况下，请不要这样做）。
我正在尝试 运行 emacs with proof generale 打开 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 一起工作有什么建议吗？
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 知道您正在编辑什么类型的文件，并且不会在编程模式下进行此类替换（除非您特意将其配置为这样做，在这种情况下，请不要这样做）。