Coq 提取：权限被拒绝

Question

当我在 CoqIDE 中执行以下命令时：

Extraction Language Haskell.
Extraction "Code.hs" my_function.

我收到以下错误：

System error: "Code.hs: Permission denied"

如果我改为尝试：

Extraction Language Haskell.
Extraction "~/Code.hs"  example10.

我收到错误：

System error: "~/Code.hs: No such file or directory"

我正在使用适用于 MacOSX 的 CoqIDE 8.5beta3。

我该如何解决这个问题？如何在没有权限问题的情况下通过 CoqIDE 进行提取？

Answer 1

您可能正在尝试写入您没有写入权限的目录，因此这不是 Coq 错误，而是您操作系统的错误。

第二个原因可能是 Coq 没有将 ~ 扩展到您的主目录。这是一种 bash 主义，而不是 OS 的东西。改为写 /Users/yourname/。