macos - 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主义，而不是操作系统的东西。/Users/yourname/改为写。