4

Я установил Coq в моей системе из установщика по умолчанию. Затем я добавил общее доказательство в мои существующие emacs. Но проблема в том, что когда я пытаюсь запустить команду в emacs, я нахожу из emacs следующее:

Поиск программы отсутствует, такой файл или каталог coqtop

Я считаю, что есть некоторые ошибки конфигурации.

Ждем ваших мыслей.

2 ответа2

1

Отличается от случая OP, но похожая проблема: Сообщение об ошибке Searching for program: no such file or directory, coqtop может также возникнуть, если вы не установили coq. Тогда команда coqtop будет отсутствовать в вашей системе.

Чтобы диагностировать, запустите which coqtop . Если результат пустой, он не установлен или не находится на вашем пути.

На Mac я решил эту проблему, установив coq с homebrew, используя brew install coq

1

Я только что понял, что мне нужно включить путь к coqtop к пути emacs. или вы можете иметь это в вашем системном пути. в этом случае вы должны вызывать Emacs из оболочки.

Всё ещё ищете ответ? Посмотрите другие вопросы с метками .