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