Search code examples
macoscoqcoqidecoq-extraction

Coq Extraction: Permission Denied

When I execute the following commands within the CoqIDE:

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

I get the following error:

System error: "Code.hs: Permission denied"

If I try instead:

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

I get the error:

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

I'm using the CoqIDE 8.5beta3 for MacOSX.

How can I fix this? How can I do extraction through the CoqIDE without having permission issues?

Solution

  • You are probably trying to write to a directory to which you don't have write permission, so it is not a Coq error, but an error from your operating system.

    The second reason is probably that Coq does not expand the ~ to your home directory. It is a bashism, not an OS thing. Write /Users/yourname/ instead.