在 emacs 中为 Coq 配置通用证明

Question

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

搜索程序没有这样的文件或目录 coqtop

我相信有一些配置错误。

期待你的想法。

Answer 1

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