Конфигурирование Proof general для Coq в emacs

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

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

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

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

Источник

4 ответа

Решение

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

Источник

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

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

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

Источник

Сначала убедитесь, что вы установили Coq (у меня сработали эти два: https://coq.inria.fr/opam-using.html или https://coq.discourse.group/t/coqtop-not-found/856/7).

Затем запросите у своего компьютера путь к текущему контейнеру дляcoqtop:

      which coqtop

например

      (base) miranda9@Brandos-MBP bin % which coqtop
/Users/miranda9/.opam/qcert-env/bin/coqtop

затем поместите этот путь в свой файл следующим образом, например:

      (setq coq-prog-name “/usr/bin/coqtop -emacs”)

На самом деле, я только что заметил, что не использовал тот, который отображается, но, похоже, он у меня все равно работает -whichхотя все равно полезно.

Дополнительные комментарии

Позвольте мне поделиться.emacsфайл, который работает для меня:

      (require 'package)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
(require 'evil)
  (evil-mode 1)
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(package-selected-packages '(proof-general)))
(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )

Я узнал, что копирование различных команд учебника не работает... например

  • если ты скопируешь(require 'package)несколько раз это вызывает ошибки, потому что это не независимая операция
  • кажется, вам не нужно явно задавать путь coqtop, если вы используете PG - PG находит его самостоятельно
    • Я думаю это потому что я установил его с опамом но это не 100%

надеюсь, это поможет.

Источник

Это сработало для меня. Я показал весь процесс от нуля до получения Coq и настройки Proof General.

Если вы хотите использовать Proof-General для Coq, сначала установите Coq или что-нибудь еще, для чего вы хотите использовать доказательство-general.

Я хотел использовать его для Coq, поэтому сначала установил Coq.

1) Установите Coq -> brew install coq(для MacOS)

Загрузите Emacs.app с https://emacsformacosx.com и установите приложение, перетащив значок в папку «Приложения».

Следуйте инструкциям по установке расширения Emacs Proof General через менеджер пакетов MELPA для Emacs или через Git.

2) Установите Proof General ->

  • Использование MELPA (рекомендуемая процедура)MELPA — это репозиторий пакетов Emacs. Пропустите этот шаг, если вы уже используете MELPA. В противном случае добавьте следующее в ваш .emacs и перезапустите Emacs:

    (требуется 'пакет) (let* ((no-ssl (и (memq system-type '(windows-nt ms-dos)) (не (gnutls-available-p)))) (прото (если нет-ssl "http" "https"))) (добавить в список архивов пакетов (cons "melpa" (concat proto "://melpa.org/packages/")) t))(package-initialize)

Примечание. Если вы переключитесь на MELPA с ранее установленного вручную Proof General, убедитесь, что вы удалили старые версии Proof General из контекста Emacs (удалив из вашего .emacs строку, загружающую PG/generic/proof-site, или удаление пакетаproofgeneral, предоставленного менеджером пакетов вашей ОС).

Затем запустите Mx package-refresh-contents RET, а затем Mx package-install RET доказательство-общее RET, чтобы установить и байт-компилировать доказательство-общее.

Теперь вы можете открыть файл Coq (.v), файл EasyCrypt (.ec) или файл PhoX (.phx), чтобы автоматически загрузить соответствующий основной режим.

  • Использование Git (процедура ручной компиляции). Удалите старые версии Proof General, клонируйте репозиторий PG с GitHub и скомпилируйте исходные коды побайтно:

    git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PGcd ~/.emacs.d/lisp/PG make

Затем добавьте в свой .emacs следующее:

      ;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

Если Proof General жалуется на несоответствие версий, убедитесь, что emacs оболочки действительно является вашим обычным Emacs. Если нет, запустите Makefile еще раз, указав явный путь к Emacs. В частности, в macOS вам, вероятно, понадобится что-то вроде

      make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

3) Добавьте следующие строки в ваш файл ~/.emacs:

      ;; Make sure we can find coqtop
(setq exec-path (append exec-path '("/usr/local/bin")))

4) Добавьте это в свой .emacs 

      (custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t))

Если вы не можете найти свой файл .emacs, проверьте это . В моем случае мне пришлось создать новый файл .emacs в моем домашнем каталоге.

Источник
Другие вопросы по тегам