0

如果我做类似的事情 -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.工作，那对我真的很有帮助。

4

1 回答 1

0

安装非系统版本 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，那么另一个将没有它们。

于 2021-01-18T20:18:47.223 回答