Я установил Coq в моей системе из установщика по умолчанию. Затем я добавил общее доказательство в мои существующие emacs. Но проблема в том, что когда я пытаюсь запустить команду в emacs, я нахожу из emacs следующее:
Поиск программы отсутствует, такой файл или каталог coqtop
Я считаю, что есть некоторые ошибки конфигурации.
Ждем ваших мыслей.
Отличается от случая OP, но похожая проблема: Сообщение об ошибке Searching for program: no such file or directory, coqtop может также возникнуть, если вы не установили coq. Тогда команда coqtop будет отсутствовать в вашей системе.
Чтобы диагностировать, запустите which coqtop . Если результат пустой, он не установлен или не находится на вашем пути.
На Mac я решил эту проблему, установив coq с homebrew, используя brew install coq
Я только что понял, что мне нужно включить путь к coqtop к пути emacs. или вы можете иметь это в вашем системном пути. в этом случае вы должны вызывать Emacs из оболочки.
