SSreflect不能与Emacs、Coq和ProofGeneral一起使用。如何在MacOS中安装SSreflect？

Question

如果我执行像- From mathcomp Require Import ssreflect.这样的操作，它会给出以下错误。

Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect

但是如果我这样做-- Require Import ssreflect.，它就会编译得很好。这可能是因为我安装了ssreflect，但并不完全是我想要的方式。

但问题是，我想要第一种工作方式，因为我有很多程序都是用这种方式编写的，而且似乎不符合逻辑地更改每个程序中的行。

这是我的.emacs文件中的内容-(我想我可能需要添加类似于mathcomp/ssreflect的路径。我不知道)

(load "~/.emacs.d/lisp/PG/generic/proof-site")

(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.
 '(coq-prog-name "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop")
 '(package-selected-packages (quote (company-coq)))
 '(proof-three-window-enable t))

;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)

如果有人能帮助我让From mathcomp Require Import ssreflect.正常工作，那将会对我很有帮助。

Answer 1

安装Coq的非系统版本的推荐方式是通过opam cf https://coq.inria.fr/opam-using.html，主要是因为它简化了软件包的安装(例如mathcomp-*软件包)，并且您可以一次只关注一个问题(coq vs emacs)。

如果您仍然决定先执行Coq的自定义安装，然后再执行mathcomp的自定义安装，请不要忘记make install步骤，该步骤会将编译的库文件复制到本地安装的子文件夹user-contrib/中。

我注意到在你最初的帖子中，你的.emacs配置文件将"/usr/local/Cellar/coq/8.10.2_1/bin/coqtop"设置为coq-prog-name，而你的终端似乎使用了/usr/local/bin/coqtop，这很可能是两个截然不同的Coq版本。所以，如果你用这个来编译和安装mathcomp，你就不会有另外一个的了。