Coq 和 Emacs：无法编译 Coq - 没有这样的文件或目录

Question

当我尝试在 Emacs 中使用 C-c 编译 Coq 文件时，出现以下错误：

    Coq compilation error: ((coqdep -Q /home/****/cs54 DMFP /tmp/ProofGeneral-coqUMWPyn.v) No such file or directory

我在 manjaro 上，通过命令行安装了 Emacs 和 Coq，但不知道发生了什么。

_CoqProject 仅包含这些字符：

   -Q . DMFP

如果这有助于缩小范围，当我在终端中输入 coqc 时，没有任何反应，提示再次出现。

当我输入 coqtop 时，程序启动，但不评估任何内容。当我输入“2”或“Check 2”之类的内容时，它只会弹出下一个输入的提示。

Answer 1

coq-prover

snap 限制对系统目录的访问，包括

/tmp

。这就是为什么

coqdep

无法处理文件

/tmp/ProofGeneral-coqUMWPyn.v

。要解决此问题，请将临时目录名称更改为 Emacs 配置中主目录的子目录：

(setq temporary-file-directory (concat (getenv "HOME") "/tmp"))