CODEWITHSUNDEEP
macoscoqcoqidecoq-extraction
Bruno
Bruno

Reputation: 864

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?

Upvotes: 0

Views: 373

Answers (1)

larsr
larsr

Reputation: 5811

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.

Upvotes: 1

Related Questions