Как установить Proof General для Emacs на Mac?

Question

Я новичок в Emacs и, возможно, в этом проблема, но я следовал инструкциям здесь:

https://github.com/ProofGeneral/PG

, в частности, после того, как я добавил указанные строки в свой .emacsфайл, который я сделал (M это клавиша alt / option):

M-x package-refresh-contents RET

но я получил сообщение об ошибке:

[no match]

что происходитне так?

---

может быть, это то, что я делаю неправильно, что означает:

 M-x package-refresh-contents RET followed by M-x package-install RET proof-general RET

значит?

Answer 1

Линия будет работать, если у вас есть melpa в качестве источника пакета.Смотрите ответ ejgallego:

 (require 'package)
 (setq package-enable-at-startup nil)
      (add-to-list 'package-archives
          '("melpa" . "https://melpa.org/packages/"))

 (package-initialize)

Если вы добавите эти строки в ваш .emacs-файл, а затем

 M-x package-refresh-contents (followed by return)
 M-x package-install (followed by return and then `proof-general`)

, тогда он будет работать без явного добавления пакета в ваш .emacs-файл.

Answer 2

Вот что у меня работает (ТМ):

(require 'package)
(setq package-enable-at-startup nil)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/"))

(package-initialize)

;; Bootstrap use-package
(unless (package-installed-p 'use-package)
    (package-refresh-contents)
    (package-install 'use-package))

(use-package proof-general
  :no-require t
  :ensure t)