☰

在 emacs 中为 Coq 配置 Proof general

tag-icon • tag-icon emacs proofing
在 emacs 中为 Coq 配置 Proof general

我从默认安装程序在系统中安装了 Coq。然后我将 proof general 添加到我现有的 emacs 中。但问题是，当我尝试在 emacs 中运行命令时，我发现 emacs 中有以下内容：

正在搜索程序没有此文件或目录 coqtop

我认为存在一些配置错误。

期待您的想法。

答案1

我刚刚发现我必须将 coqtop 的路径包含在 emacs 路径中。或者您可以将其放在系统路径中。在这种情况下，您必须从 shell 调用 emacs。

答案2

与 OP 的情况不同，但问题类似：Searching for program: no such file or directory, coqtop如果您尚未安装 coq，也可能会出现错误消息。然后coqtop您的系统将会缺少命令。

要进行诊断，请运行which coqtop。如果结果为空，则表示未安装或不在您的路径上。

在 Mac 上，我通过安装 coq 解决了这个问题自制使用brew install coq

答案3

这对我有用。我展示了从零开始获取 Coq 并配置 Proof General 的整个过程。

如果您想将 Proof-General 用于 Coq，请首先安装 Coq 或您想要使用 proof-general 的任何内容。

我想将它用于 Coq，所以我首先安装了 Coq。

1） 安装 Coq -> brew install coq（适用于 macOS）

获取 Emacs.app从https://emacsformacosx.com并通过将图标拖拽到应用程序文件夹中来安装该应用程序。

按照说明通过 Emacs 的 MELPA 包管理器或 Git 安装 Emacs Proof General 扩展。

2） 安装证明常规 ->

  • 使用 MELPA（推荐程序） MELPA 是 Emacs 软件包的存储库。如果您已经使用 MELPA，请跳过此步骤。否则，将以下内容添加到您的 .emacs 并重新启动 Emacs：

    (require'包) (let*((no-ssl(and(memq system-type'(windows-nt ms-dos))(not(gnutls-available-p)))) (proto(if no-ssl"http""https"))) (add-to-list'包档案(cons"melpa"(concat proto"://melpa.org/packages/"))t)) (包初始化)

注意：如果您从之前手动安装的 Proof General 切换到 MELPA，请确保从 Emacs 上下文中删除了旧版本的 Proof General（通过从 .emacs 中删除加载 PG/generic/proof-site 的行，或通过卸载 OS 包管理器提供的 proofgeneral 包）。

然后，运行 Mx package-refresh-contents RET，接着运行 Mx package-install RET proof-general RET 来安装并字节编译 proof-general。

您现在可以打开 Coq 文件 (.v)、EasyCrypt 文件 (.ec) 或 PhoX 文件 (.phx) 以自动加载相应的主模式。

  • 使用 Git（手动编译程序） 删除旧版本的 Proof General，从 GitHub 克隆 PG repo 并对源代码进行字节编译：

    git 克隆https://github.com/ProofGeneral/PG~/.emacs.d/lisp/PG cd ~/.emacs.d/lisp/PG make

然后将以下内容添加到您的 .emacs：

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

如果 Proof General 抱怨版本不匹配，请确保 shell 的 emacs 确实是您常用的 Emacs。如果不是，请使用 Emacs 的明确路径再次运行 Makefile。特别是在 macOS 上，您可能需要类似

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

3）将以下行添加到您的〜/.emacs文件：

;; Make sure we can find coqtop
(setq exec-path (append exec-path '("/usr/local/bin")))

4）将其添加到你的 .emacs

(custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t))

如果你找不到你的 .emacs 文件，请检查这就我而言，我必须在我的主目录中创建一个新的 .emacs 文件。

答案4

首先确保你已经安装了 Coq（这两个对我来说很有用：https://coq.inria.fr/opam-using.html或者https://coq.discourse.group/t/coqtop-not-found/856/7）。

然后向您的计算机询问当前 bin 的路径coqtop：

which coqtop

例如

(base) miranda9@Brandos-MBP bin % which coqtop
/Users/miranda9/.opam/qcert-env/bin/coqtop

然后将该路径放入您的.emacs文件中，如下所示：

(setq coq-prog-name “/usr/bin/coqtop -emacs”)

实际上，我刚刚注意到我没有使用所显示的那个，which但无论如何它似乎对我有用 -which但仍然有用。

补充评论

让我分享.emacs对我有用的文件：

(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)
(require 'evil)
  (evil-mode 1)
(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.
 )

我了解到复制粘贴不同的教程命令效果不佳……例如

  • 如果你复制(require 'package)多次，就会导致错误，因为它不是一个独立的操作
  • 如果你使用 PG，似乎不需要明确设置 coqtop 路径 - PG 会自行找到它
    • 我想这是因为我用 opam 安装了它，但我不是 100%

希望有帮助。

相关内容