时间戳

首页 > 解决方案 > 在打开 emacs 时添加到 coqtop 的路径时，“符号的值作为变量是无效的”

emacs - 在打开 emacs 时添加到 coqtop 的路径时，“符号的值作为变量是无效的”

问题描述

我正在尝试运行带有一般证明的 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 一起工作的任何建议？

标签： emacscoqproof-general

解决方案

推荐阅读