0

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 を介して抽出を行うにはどうすればよいですか?

4

1 に答える 1