SSreflect не работает с Emacs, Coq и ProofGeneral. Как установить SSreflect в MacOS?

Если я делаю что-то вроде - From mathcomp Require Import ssreflect., это дает мне следующую ошибку.

Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect

Но если я сделаю это вместо этого - Require Import ssreflect. компилируется просто отлично. Вероятно, это потому, что у меня установлен ssreflect, но не совсем так, как я хочу.

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

Это то, что у меня есть в моем файле .emacs (я думаю, может быть, мне нужно добавить что-то вроде пути к mathcomp/ssreflect.. Я не знаю)

(load "~/.emacs.d/lisp/PG/generic/proof-site")

(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.
 '(coq-prog-name "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop")
 '(package-selected-packages (quote (company-coq)))
 '(proof-three-window-enable t))

;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)

Мне было бы очень полезно, если бы кто-нибудь помог мне заставить From mathcomp Require Import ssreflect. работать.


path emacs coq ssreflect proof-general
person Vedant Chavda    schedule 11.03.2020    source источник
comment
Я попытался составить рецепт для студентов, которые посещают мои занятия на Coq, похоже, у них это сработало: >gist.github.com/anton-trunov/4798b61868e970b5b529951fec9ac3f2   -  person Anton Trunov    schedule 11.03.2020
comment
Спасибо Антон. Я пробовал следовать обоим методам, перечисленным в MacOS, но после попытки From mathcomp Require Import ssreflect в CoqIDE выдает следующую ошибку: Cannot find a physical path bound to logical path matching suffix <> and prefix mathcomp.   -  person Vedant Chavda    schedule 12.03.2020
comment
Однако, если я запускаю coqtop со своего терминала, From mathcomp Require Import ssreflect работает. Это также работает, если я запишу его в файл .v и скомпилирую на терминале, используя coqc name.v. Однако это не работает при работе с Emacs (вместе с Proof General). Возможно ли, что версии Coq, используемые в терминале и Emacs, отличаются?   -  person Vedant Chavda    schedule 12.03.2020
comment
Да, необходима некоторая конфигурация, чтобы заставить Emacs использовать настройки системной оболочки. К сожалению, я не помню подробностей (сейчас я использую Spacemacs), но это должно быть доступно для поиска.   -  person Anton Trunov    schedule 12.03.2020
comment
Привет, @VedantChavda, возможно, у тебя неправильно установлен ssreflect: кажется, что последние версии Coq поставляются в комплекте с ssreflect частью ssreflect, но не со всем mathcomp. Чтобы попробовать, попробуйте запросить другой файл, например tuple, ssrnat и т. д.   -  person Ptival    schedule 12.03.2020
comment
Ты прав @Ptival. From mathcomp Require Import ssrnat и Require Import ssrnat не работают в Emacs. (Хотя From mathcomp Require Import ssrnat работает в coqtop в терминале). Но Require Import ssreflect работает. Что я должен делать? Также обратите внимание, что моя проблема заключается не только в том, чтобы установить ssreflect, но и в том, чтобы установить его таким образом, чтобы From mathcomp Require Import ssreflect компилировалось.   -  person Vedant Chavda    schedule 12.03.2020
comment
Вы уверены, что у вас установлена ​​только одна версия Coq и что версия, которую запускает emacs, такая же, как и в вашем терминале? (Интересно, установлен ли у вас mathcomp для одной версии Coq, но не для другой, например)   -  person Ptival    schedule 12.03.2020
comment
Я думаю, что у меня может быть установлено несколько версий, но как мне проверить? И как узнать, какая версия coq Emacs используется? Обе команды which coqc и which coqtop в терминале дают /usr/local/bin/coqtop or coqc в качестве вывода. Возможно, у меня установлен mathcomp для одной версии, но я понятия не имею, какой именно. Дело в том, что, поскольку я новичок в этом, я пытался много искать и пробовать различные способы установки, поэтому в процессе я мог установить несколько версий и, возможно, перепутал, какую версию использует Emacs. имеет mathcomp и т. д.   -  person Vedant Chavda    schedule 12.03.2020
comment
Также я попробовал gist.github.com/anton-trunov/b55fae56f92c35531fc480232bc74160 по этой ссылке (от @AntonTrunov), в котором показано, как переключаться между версиями в Emacs. Но я не совсем уверен, как это использовать. Я сделал M-x coq-change-compiler, а затем попытался ввести /usr/local/bin, когда он запросил Compiler : , но после этого Emacs все еще не компилировал From mathcomp Require Import ssrnat.   -  person Vedant Chavda    schedule 12.03.2020

Ответы (1)


arrow_upward
0
arrow_downward

Рекомендуемый способ установки несистемных версий Coq — через opam cf https://coq.inria.fr/opam-using.html, главным образом потому, что он упрощает установку пакетов (например, пакетов mathcomp-*), и вы можете сосредоточиться на одной проблеме за раз (coq или emacs).

Если вы все же решите выполнить выборочную установку Coq, а затем mathcomp, не забудьте шаг make install, который предполагает копирование скомпилированных файлов библиотеки в подпапку user-contrib/ вашей локальной установки.

Я заметил, что в вашем исходном сообщении ваш файл конфигурации .emacs устанавливает "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop" как coq-prog-name, в то время как ваш терминал, похоже, использует /usr/local/bin/coqtop, что вполне может быть двумя разными версиями Coq. Поэтому, если вы скомпилировали и установили mathcomp с помощью этого, у вас их не будет для другого.

person Cyril    schedule 18.01.2021