Извлечение 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"

Я использую CoqIDE 8.5beta3 для MacOSX.

Как я могу это исправить? Как я могу сделать извлечение через CoqIDE без проблем с разрешением?

Answer 1

Возможно, вы пытаетесь выполнить запись в каталог, в который у вас нет разрешения на запись, поэтому это не ошибка Coq, а ошибка вашей операционной системы.

Вторая причина, вероятно, заключается в том, что Coq не расширяет ~ в ваш домашний каталог. Это bashИзм, не вещь ОС. Написать /Users/yourname/ вместо.